√2 continued-fraction convergents
Theorem.√2 continued-fraction convergents — the [1;2,2,2,…] convergents 1/1, 3/2, 7/5, 17/12, 41/29, … are best rational approximations (|p/q − √2| < 1/q²) and satisfy p² − 2q² = ±1, for the first 17.
Proof.the [1;2,2,2,…] convergents 1/1, 3/2, 7/5, 17/12, 41/29, … are best rational approximations (|p/q − √2| < 1/q²) and satisfy p² − 2q² = ±1, for the first 17.
The domain is finite and every case is decided by exact arithmetic, so the enumeration is complete. ∎
src/9/1/index.ts#discoveredTheoremsWaveThirtyTwo
Figure — the proof, computed and plotted
pₖ = 2pₖ₋₁ + pₖ₋₂, qₖ = 2qₖ₋₁ + qₖ₋₂ (√2 = [1; 2,2,2,…]), pₖ² − 2qₖ² = ±1
Computed by Pell recurrence, exact integers — recomputed on every build, zero tokens.
1 · Classification
finite-complete — self-contained computation, no external lean
2 · Provenance
Documented theorem re-derived by exhaustive computation (humanityNovel=false); first-in-this-registry is the only sense of discovered.
Acknowledgment
"√2 continued-fraction convergents" is a re-derivation, acknowledged to documented mathematics — the original proof is the prior art this re-derivation acknowledges; not new to humanity — the contribution is the reproducible computation discoveredTheoremsWaveThirtyTwo.
- Prior art
- documented mathematics — the original proof is the prior art this re-derivation acknowledges
- Novelty
- not new to humanity — a re-derivation (humanityNovel = false)
- Contribution
- a reproducible computation (discoveredTheoremsWaveThirtyTwo @ src/9/1) that re-derives the result at zero tokens — the contribution is the verifiable recomputation, NOT the theorem
3 · Reproducibility
Recompute from source: npm run theorems:verify recomputes discoveredTheoremsWaveThirtyTwo (src/9/1/index.ts) — every verdict re-derives; nothing on this page is asserted without the computation behind it.