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

Determinant identity for consecutive convergents

Statement

Let $p_{n} / q_{n}$ be the convergents of a regular continued fraction. Then for every $n \geq 0$ , $p_{n} q_{n - 1} - p_{n - 1} q_{n} = (- 1)^{n - 1} .$ Consequently, for every $n \geq 1$ , $\frac{p_{n}}{q_{n}} - \frac{p_{n - 1}}{q_{n - 1}} = \frac{(- 1)^{n - 1}}{q_{n} q_{n - 1}} .$

Facts & Assumptions

Given: A regular continued fraction with convergent sequences $p_{n}, q_{n}$ .

[F1]

The convergents satisfy $p_{- 2} = 0$ , $p_{- 1} = 1$ , $q_{- 2} = 1$ , $q_{- 1} = 0$ , and $p_{n} = a_{n} p_{n - 1} + p_{n - 2}$ , $q_{n} = a_{n} q_{n - 1} + q_{n - 2}$ for $n \geq 0$ . (Convergents of a regular continued fraction).

[F2]

If a subset of $N$ contains $0$ and is closed under successor, then it is all of $N$ (The principle of mathematical induction).

Proof

technique · direct

1.1

At $n = 0$ one has. [given, F1, base, algebra] $p_{0} q_{- 1} - p_{- 1} q_{0} = a_{0} \cdot 0 - 1 \cdot 1 = - 1 = (- 1)^{- 1} .$

givenF1basealgebra

1.2

If $D_{n} : = p_{n} q_{n - 1} - p_{n - 1} q_{n}$ , then the recurrences of [F1] give. [F1, induction, algebra] $D_{n + 1} = (a_{n + 1} p_{n} + p_{n - 1}) q_{n} - p_{n} (a_{n + 1} q_{n} + q_{n - 1}) = - D_{n} .$ So the sign flips at each successor step.

F1inductionalgebra

2.1

Steps 1.1 and 1.2 imply by induction that. [F2, step 1.1, step 1.2, discharge-induction] $D_{n} = (- 1)^{n - 1}$ for every $n \geq 0$ .

F2step 1.1step 1.2discharge-induction

3.1

For $n \geq 1$ . [step 2.1, algebra] $\frac{p_{n}}{q_{n}} - \frac{p_{n - 1}}{q_{n - 1}} = \frac{p_{n} q_{n - 1} - p_{n - 1} q_{n}}{q_{n} q_{n - 1}} = \frac{(- 1)^{n - 1}}{q_{n} q_{n - 1}}$ by step 2.1.

step 2.1algebra∎

Depends on

Used by

Dependency tree · two levels

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