Alphabeta Math
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.

Determinant identity for consecutive convergents

Statement

Let pn/qn be the convergents of a regular continued fraction. Then for every n≥0, pnqn−1−pn−1qn=(−1)n−1. Consequently, for every n≥1, pnqn−pn−1qn−1=(−1)n−1qnqn−1.

Facts & Assumptions

Given: A regular continued fraction with convergent sequences pn,qn.

[F1]

The convergents satisfy p−2=0, p−1=1, q−2=1, q−1=0, and pn=anpn−1+pn−2, qn=anqn−1+qn−2 for n≥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.1givenF1basealgebra

At n=0 one has. [given, F1, base, algebra] p0q−1−p−1q0=a0⋅0−1⋅1=−1=(−1)−1.

1.2F1inductionalgebra

If Dn:=pnqn−1−pn−1qn, then the recurrences of [F1] give. [F1, induction, algebra] Dn+1=(an+1pn+pn−1)qn−pn(an+1qn+qn−1)=−Dn. So the sign flips at each successor step.

2.1F2step 1.1step 1.2discharge-induction

Steps 1.1 and 1.2 imply by induction that. [F2, step 1.1, step 1.2, discharge-induction] Dn=(−1)n−1 for every n≥0.

3.1step 2.1algebra∎

For n≥1. [step 2.1, algebra] pnqn−pn−1qn−1=pnqn−1−pn−1qnqnqn−1=(−1)n−1qnqn−1 by step 2.1.

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