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 terminates exactly on rational numbers

Statement

For a real number $α$ , the continued-fraction algorithm terminates if and only if $α$ is rational. When $α$ is rational, the continued-fraction digits are exactly the successive quotient digits of the Euclidean algorithm.

Facts & Assumptions

Given: A real number $α$ and its continued-fraction algorithm.

[F1]

If $u, v \in Z$ with $v > 0$ , then there are unique integers $a, r$ with $u = a v + r, 0 \leq r < v .$ (Division with remainder in $Z$ : for $a \in Z$ and $b > 0$ there are unique $q, r \in Z$ with $a = q b + r$ and $0 \leq r < b$ ).

[F2]

A terminating continued-fraction expansion is a finite regular continued fraction, and every finite regular continued fraction equals its last convergent $p_{n} / q_{n} \in Q$ (The continued-fraction algorithm for real numbers, Convergents are given by the standard recurrences and tail formula).

[F3]

Every complete quotient after the first is greater than $1$ (Complete quotients in the continued-fraction algorithm).

Proof

technique · direct

1.1givenF1algebra

If $α$ is an integer, the algorithm stops immediately. Otherwise write $α = u_{0} / v_{0}$ with integers $v_{0} > 0$ and $\gcd (u_{0}, v_{0}) = 1$ . Applying [F1] to. [given, F1, algebra] $u_{0}$ and $v_{0}$ gives $u_{0} = a_{0} v_{0} + r_{0}, 0 < r_{0} < v_{0},$ so $α = a_{0} + \frac{r_{0}}{v_{0}}, α_{1} = \frac{1}{α - a_{0}} = \frac{v_{0}}{r_{0}} .$ Thus the next numerator is the previous denominator.

1.2F2

Conversely, if the algorithm terminates, then by [F2] the original number is a finite regular continued fraction and hence rational.

1.3F1F3inductionalgebra

Let $n \geq 1$ , and suppose. [F1, F3, induction, algebra] $α_{n} = \frac{u_{n}}{v_{n}} (v_{n} > 0, \gcd (u_{n}, v_{n}) = 1)$ is not an integer. Since $n \geq 1$ , fact [F3] gives $α_{n} > 1$ , so $u_{n} > v_{n} > 0$ . Applying [F1] gives $u_{n} = a_{n} v_{n} + r_{n}, 0 < r_{n} < v_{n}, α_{n + 1} = \frac{v_{n}}{r_{n}} .$ Any common divisor of $v_{n}$ and $r_{n} = u_{n} - a_{n} v_{n}$ also divides $u_{n}$ , so $\gcd (v_{n}, r_{n}) = 1$ . Hence this is already the reduced form $α_{n + 1} = \frac{u_{n + 1}}{v_{n + 1}} = \frac{v_{n}}{r_{n}},$ and therefore $u_{n + 1} = v_{n} < u_{n}$ .

2.1step 1.1step 1.3induction

When $α$ is a nonintegral rational, step 1.1 gives $α_{1} = \frac{v_{0}}{r_{0}} > 1.$ So step 1.3 applies successively to $α_{1}, α_{2}, \dots$ as long as they remain nonintegral. Their positive integer numerators $u_{1}, u_{2}, u_{3}, \dots$ then form a strictly decreasing sequence, which cannot continue forever. Therefore some complete quotient is an integer, and the algorithm terminates.

3.1step 1.1step 1.3F1∎

The equations in steps 1.1 and 1.3 are exactly the Euclidean divisions of the successive numerator-denominator pairs, so the continued-fraction digits are. [step 1.1, step 1.3, F1] the Euclidean quotient digits.

Depends on

Used by

Dependency tree · two levels

26 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)