Reverse Euclidean history · forward quotient list · Constructive arithmetic

Finite simple continued fractions

a,b > 0 → ∃s. ContinuedFraction(a,b,s)

Nine independently checked Heyting-arithmetic proofs build a complete beta-coded Euclidean history and prove existence of a nonempty simple continued fraction for every pair of positive naturals.

Open the definition-aware map Read the final theorem See campaign milestone G071

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Exact certificate

Fully expanded arithmetic

Inspect all 381 native tactic lines and 25 actual proof prerequisites with every definition fully expanded.

Open the exact edition →

Focused route

Final dependency cone

Start at theorem CF0009 and follow only the lemmas and conservative definitions supporting continued_fraction_positive_exists.

Trace prerequisites →
Zoom between mathematical scales: complete research atlas → research domain → proof family → G071 milestone → theorem and definition dependencies.
Major independently established statements: CF0008 continued_fraction_positive_nonempty_exists · CF0009 continued_fraction_positive_exists.
Independently verified Alpha v34 checked-use theorem family: 9 dependency-curried kernel-checked theorem bodies · 25 proof prerequisites · 5 linked definitions · 4 definition-dependency arrows · 381 exact tactic lines · first admitted v20 · not Stable. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 590 bundle nodes; SHA-256 1b623064f36e362c1a117daa193b1ee33ee7905ec804ee1ac164b42345b67069.
Exact mathematical boundary: Every displayed theorem was first admitted in Alpha v20, remains independently kernel- and Lean-verified for current Alpha v30 checked use, and has not been promoted to Stable.