Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-27
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Every infinite regular continued fraction converges to a unique real number

Statement

Let [a0;a1,a2,] be an infinite regular continued fraction, and let cn:=pn/qn be its convergents. Then:

  1. c0<c2<c4< and c1>c3>c5>;
  2. every even convergent is below every odd convergent; and
  3. there is a unique real number x such that both subsequences (c2m)m0 and (c2m+1)m0 converge to x.

This real number is the value of the infinite regular continued fraction.

Facts & Assumptions

Given: An infinite regular continued fraction and its convergents cn=pn/qn.

[F1]

Consecutive convergents satisfy cncn1=(1)n1qnqn1 for n1 (Determinant identity for consecutive convergents).

[F2]

Every complete ordered field is Archimedean (Every complete ordered field is Archimedean).

Proof

technique · direct
1.1

Since every partial quotient after the first is at least 1. [given, F1, induction, algebra] The denominators satisfy qn+1=an+1qn+qn1qn+qn1>qn>0 for n1, with q0=1 and q1=a11. Thus (qn) is nondecreasing from q0 onward and strictly increasing from q1 onward, and induction on n gives qnn for n1.

givenF1inductionalgebra
2.1

By [F1], the signs of cncn1 alternate, and by step 1.1 their absolute values strictly decrease. [F1, step 1.1, algebra] Hence c2m<c2m+1,c2m+2=c2m+1(c2m+1c2m+2)>c2m, and similarly c2m+3=c2m+2(c2m+2c2m+3)<c2m+1. So the even convergents increase, the odd convergents decrease, and every even convergent is below every odd convergent.

F1step 1.1algebra
2.2

Put dn:=1/(qnqn+1). [F2, step 1.1, algebra] Step 1.1 gives dn1/(n(n+1)) for n1, and the Archimedean property [F2] therefore implies dn0. For ε>0 choose N1 with 1/N<ε, then for nN, 0<dn1n(n+1)1n1N<ε.

F2step 1.1algebra
3.1

Let E:={c2m:m0}. [step 2.1, given] By step 2.1 the set E is nonempty and bounded above by c1, so [F3] gives a real number x:=supE.

step 2.1given
3.2

If n=2m+1 is odd, then cn1E and step 2.1 gives. [step 2.1, step 2.2, F1] cn1xcn, so 0cnxcncn1=dn1. If n=2m is even, then cnE and step 2.1 gives cnxcn+1, so 0xcncn+1cn=dn. Since the right-hand sides tend to 0 by step 2.2, both subsequences converge to x.

step 2.1step 2.2F1
4.1

If y were another real with both subsequences converging to y, then for every m. [step 3.2, algebra] xyxc2m+c2my, and the right-hand side tends to 0 as m by step 3.2. Hence x=y, so the value is unique.

step 3.2algebra

Depends on

Used by

Dependency tree · two levels

22 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources