CorollaryStatement: Literature-sourcedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (gpt-5.6-terra)audited 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.

Convergents are reduced fractions

Statement

Every convergent $p_{n} / q_{n}$ of a regular continued fraction is in lowest terms. Moreover, for each $n \geq 0$ the two vectors $(q_{n}, p_{n}), (q_{n + 1}, p_{n + 1})$ form a $Z$ -basis of $Z^{2}$ .

Facts & Assumptions

Given: A regular continued fraction and its convergents $p_{n} / q_{n}$ .

[F1]

Consecutive convergents satisfy $p_{n} q_{n - 1} - p_{n - 1} q_{n} = (- 1)^{n - 1}$ for $n \geq 0$ . (Determinant identity for consecutive convergents).

[F2]

If integers $a, b$ are not both $0$ , then $\gcd (a, b)$ is an integer linear combination of $a$ and $b$ (Bézout's identity: for integers $a, b$ not both zero, $\gcd (a, b)$ is the least positive element of ${a x + b y : x, y \in Z}$ ; in particular $a x + b y = \gcd (a, b)$ has an integer solution).

Proof

technique · direct

1.1

Let $d$ be a common divisor of $p_{n}$ and $q_{n}$ . [F1, F2, given] Then $d$ divides every integer linear combination of $p_{n}$ and $q_{n}$ , in particular $p_{n} q_{n - 1} - p_{n - 1} q_{n} = (- 1)^{n - 1}$ by [F1]. Hence $d$ divides $1$ , so $d = 1$ and $p_{n} / q_{n}$ is reduced.

F1F2given

1.2

The determinant of the matrix with columns $(q_{n}, p_{n})$ and $(q_{n + 1}, p_{n + 1})$ is. [F1, algebra] $q_{n} p_{n + 1} - p_{n} q_{n + 1} = (- 1)^{n}$ by [F1]. Therefore $(\begin{array}{c} u \\ v \end{array}) = (- 1)^{n} (u p_{n + 1} - v q_{n + 1}) (\begin{array}{c} q_{n} \\ p_{n} \end{array}) + (- 1)^{n} (v q_{n} - u p_{n}) (\begin{array}{c} q_{n + 1} \\ p_{n + 1} \end{array})$ for every $(u, v) \in Z^{2}$ , so the two columns span $Z^{2}$ over $Z$ .

F1algebra

2.1

Steps 1.1 and 1.2 are exactly the two assertions.

step 1.1step 1.2∎

Depends on

Used by

Convergents are best rational approximations of the first kind Theorem

Dependency tree · two levels

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