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.

Normalized finite regular continued fractions are unique

Statement

Every rational number has a unique normalized finite regular continued fraction: either the expansion has length $0$ , or its last digit is at least $2$ . If the rational is not an integer, then it has exactly one other finite regular continued-fraction expansion, obtained by replacing the last digit $a_{n} \geq 2$ by the pair $a_{n} - 1, 1$ . An integer $m$ has exactly the two expansions $[m]$ and $[m - 1; 1]$ .

Facts & Assumptions

Given: A rational number and its finite regular continued-fraction expansions.

[F1]

The continued-fraction algorithm terminates exactly on rational numbers, and its digit list is the Euclidean-algorithm digit list. (The continued-fraction algorithm terminates exactly on rational numbers).

[F2]

For every finite regular continued fraction, $[a_{0}; a_{1}, \dots, a_{n}, t] = \frac{t p_{n} + p_{n - 1}}{t q_{n} + q_{n - 1}},$ so in particular $[a_{0}; a_{1}, \dots, a_{n}, 1] = [a_{0}; a_{1}, \dots, a_{n} + 1] .$ (Convergents are given by the standard recurrences and tail formula).

Proof

technique · direct

1.1

By [F1], every rational number has a terminating continued-fraction expansion. If the rational is not an integer, the last complete quotient is a positive integer greater than $1$ . [F1, given] Because every complete quotient after the first is greater than $1$ , the algorithm already produces a normalized finite expansion.

F1given

1.2

If $a_{n} \geq 2$ , then [F2] gives. [F2, algebra] $[a_{0}; a_{1}, \dots, a_{n}] = [a_{0}; a_{1}, \dots, a_{n} - 1, 1] .$ For an integer $m$ , the same identity reads $[m] = [m - 1, 1] = [m - 1; 1] .$ So every normalized finite expansion produces a second finite expansion.

F2algebra

1.3

Conversely, any finite expansion with last digit $1$ and length at least $1$ can be shortened by the identity. [F2, induction] $[a_{0}; a_{1}, \dots, a_{n - 1}, 1] = [a_{0}; a_{1}, \dots, a_{n - 1} + 1] .$ Repeating this collapse removes every terminal $1$ and ends at a normalized expansion. Thus every finite expansion is obtained from a normalized one by at most one final split of the last digit.

F2induction

2.1

The normalized expansion is unique because the continued-fraction algorithm on a rational has unique digits at each step. [F1, step 1.2, step 1.3] Each digit is the unique integer part of the current complete quotient, and [F1] says the process terminates. Therefore nonintegers have exactly two finite expansions, while integers have exactly the two listed in step 1.2.

F1step 1.2step 1.3∎

Depends on

Used by

A rational number has exactly two finite regular continued-fraction expansions Example

Dependency tree · two levels

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