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 be an infinite regular continued fraction, and let be its convergents. Then:
- and ;
- every even convergent is below every odd convergent; and
- there is a unique real number such that both subsequences and converge to .
This real number is the value of the infinite regular continued fraction.
Facts & Assumptions
Given: An infinite regular continued fraction and its convergents .
Consecutive convergents satisfy for (Determinant identity for consecutive convergents).
Every complete ordered field is Archimedean (Every complete ordered field is Archimedean).
The constructed real field has the least-upper-bound property (The Cauchy-sequence reals have the least-upper-bound property, Complete ordered field (least-upper-bound property)).
Proof
Since every partial quotient after the first is at least . [given, F1, induction, algebra] The denominators satisfy for , with and . Thus is nondecreasing from onward and strictly increasing from onward, and induction on gives for .
By [F1], the signs of alternate, and by step 1.1 their absolute values strictly decrease. [F1, step 1.1, algebra] Hence and similarly So the even convergents increase, the odd convergents decrease, and every even convergent is below every odd convergent.
Put . [F2, step 1.1, algebra] Step 1.1 gives for , and the Archimedean property [F2] therefore implies . For choose with , then for ,
Let . [step 2.1, given] By step 2.1 the set is nonempty and bounded above by , so [F3] gives a real number .
If is odd, then and step 2.1 gives. [step 2.1, step 2.2, F1] , so If is even, then and step 2.1 gives , so Since the right-hand sides tend to by step 2.2, both subsequences converge to .
If were another real with both subsequences converging to , then for every . [step 3.2, algebra] and the right-hand side tends to as by step 3.2. Hence , so the value is unique.
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
- Peter Hackman, Elementary Number Theory (standard reference, not scraped)
- William Stein, Elementary Number Theory: Primes, Congruences, and Secrets (standard reference, not scraped)