Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedprecheck 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.

The continued-fraction algorithm for real numbers

Statement

Let α be a real number. The complete-quotient algorithm of Complete quotients in the continued-fraction algorithm either terminates with a finite regular continued fraction equal to α, or produces an infinite regular continued fraction whose convergents converge to α.

Facts & Assumptions

Given: A real number α, its complete quotients αn, its digits an, and its convergents pn/qn.

[F1]

Whenever αn+1 is defined, α=αn+1pn+pn−1αn+1qn+qn−1. (Complete-quotient tail formula).

[F2]

Consecutive convergents satisfy pnqn−1−pn−1qn=(−1)n−1. (Determinant identity for consecutive convergents).

[F3]

Every infinite regular continued fraction has a unique value, namely the common limit of its even and odd convergent subsequences. (Every infinite regular continued fraction converges to a unique real number).

Proof

technique · direct
1.1givenalgebra

If αN=aN for some N, then repeated substitution of the identities αn=an+1/αn+1 for n<N yields. [given, algebra] α=[a0;a1,…,aN]. For N≥1 the last digit aN=αN is positive because every complete quotient after the first is greater than 1, so the output is a finite regular continued fraction.

1.2F1F2algebra

Suppose the algorithm never terminates. Then every αn+1 is defined and satisfies αn+1>an+1≥1, so [F1] and [F2] give. [F1, F2, algebra] α−pnqn=pn−1qn−pnqn−1qn(αn+1qn+qn−1)=(−1)nqn(αn+1qn+qn−1). Hence ∣α−pnqn∣<1qn(an+1qn+qn−1)=1qnqn+1.

2.1F3step 1.2algebra

The infinite digit sequence a0,a1,… is therefore a regular continued fraction, so by [F3] its convergents pn/qn converge to some real number x. [F3, step 1.2, algebra] Step 1.2 shows α−pn/qn→0, and therefore ∣α−x∣≤∣α−pnqn∣+∣pnqn−x∣→0. Thus α=x.

3.1step 1.1step 2.1∎

Step 1.1 handles the terminating case and step 2.1 the nonterminating case, so the algorithm always reconstructs the original real number.

Depends on

Used by

Dependency tree · two levels

13 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