LemmaStatement: 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.

Convergent error bound

Statement

Let $α$ be an irrational real number, and let $p_{n} / q_{n}$ be its continued- fraction convergents. Then, for every $n \geq 0$ , $∣ α - \frac{p_{n}}{q_{n}} ∣ < \frac{1}{q_{n} q_{n + 1}} \leq \frac{1}{q_{n}^{2}} .$ Moreover, $α - \frac{p_{n}}{q_{n}}$ has sign $(- 1)^{n}$ , so the convergents alternate around $α$ .

Facts & Assumptions

Given: An irrational real number $α$ , its continued-fraction digits $a_{n}$ , its complete quotients $α_{n}$ , and its convergents $p_{n} / q_{n}$ .

[F1]

An irrational real does not terminate under the continued-fraction algorithm, so every complete quotient $α_{n + 1}$ is defined and $α = \frac{α_{n + 1} p_{n} + p_{n - 1}}{α_{n + 1} q_{n} + q_{n - 1}} .$ (The continued-fraction algorithm terminates exactly on rational numbers, Complete-quotient tail formula).

[F2]

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

[F3]

The convergent denominators satisfy $q_{- 1} = 0$ , are positive for every index $n \geq 0$ , and obey $q_{n + 1} = a_{n + 1} q_{n} + q_{n - 1}$ (Convergents of a regular continued fraction).

[F4]

For irrational $α$ , the algorithm does not terminate, so $α_{n + 1} \neq a_{n + 1}$ ; the defining floor inequality therefore gives $1 \leq a_{n + 1} < α_{n + 1}$ (The continued-fraction algorithm terminates exactly on rational numbers, Complete quotients in the continued-fraction algorithm).

Proof

technique · direct

1.1F1F2F3F4algebra

By [F1] and [F2]. [F1, F2, F3, F4, algebra] $α - \frac{p_{n}}{q_{n}} = \frac{q_{n} (α_{n + 1} p_{n} + p_{n - 1}) - p_{n} (α_{n + 1} q_{n} + q_{n - 1})}{q_{n} (α_{n + 1} q_{n} + q_{n - 1})} = \frac{(- 1)^{n}}{q_{n} (α_{n + 1} q_{n} + q_{n - 1})} .$ The denominator is positive by [F3] and [F4], so the sign is $(- 1)^{n}$ .

2.1step 1.1F3F4algebra

Fact [F4] gives $α_{n + 1} > a_{n + 1}$ , and [F3] gives. [step 1.1, F3, F4, algebra] $α_{n + 1} q_{n} + q_{n - 1} > a_{n + 1} q_{n} + q_{n - 1} = q_{n + 1} .$ Taking absolute values in step 1.1 yields $∣ α - \frac{p_{n}}{q_{n}} ∣ < \frac{1}{q_{n} q_{n + 1}} .$

3.1F3F4step 2.1algebra∎

Facts [F3] and [F4] give $q_{n + 1} \geq q_{n} > 0$ , so the second inequality is immediate. [F3, F4, step 2.1, algebra] $\frac{1}{q_{n} q_{n + 1}} \leq \frac{1}{q_{n}^{2}}$

Depends on

Used by

Dependency tree · two levels

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