Finite simple continued fractions — Exact Proof Explorer

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.

9 theorem bodies · 25 proof edges · 381 tactic lines · 7 layers

Alpha v34 checked-use · first admitted v20 · independently kernel and Lean verified; not Stable

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.

9 theorems
0123456
CF0002 · continued_fraction_empty_trace

The zero-divisor Euclidean base case has exactly the empty quotient list and no transitions.

layer 0 · 16 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable
CF0003 · continued_fraction_empty_trace_exists

For every dividend, a fully witnessed empty reverse Euclidean history exists at divisor zero.

layer 1 · 8 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable
CF0004 · continued_fraction_trace_extend

A strict Euclidean division prepends its quotient and extends one beta-coded history without changing any earlier state.

layer 0 · 133 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable
CF0005 · continued_fraction_trace_exists_up_to

Bounded natural induction terminates Euclid at zero and builds a complete forward quotient list for every divisor below its bound.

layer 2 · 100 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable
CF0006 · continued_fraction_trace_exists

Every pair of natural numbers, including zero-input boundaries, has a finite completely witnessed Euclidean quotient trace.

layer 3 · 11 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable
CF0007 · continued_fraction_nonzero_divisor_exists

Every nonzero divisor produces a strictly positive trace length and a genuinely nonempty forward quotient list.

layer 4 · 49 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable
CF0008 · continued_fraction_positive_nonempty_exists

Every positive rational input has a complete simple continued fraction whose exact cell-coded quotient list is nonempty.

layer 5 · 39 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable
CF0009 · continued_fraction_positive_exists

G071: every pair of strictly positive naturals admits its complete witnessed finite simple continued-fraction quotient list.

layer 6 · 14 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

Exactly 9 displayed theorems have independently verified Alpha checked-use authority; none is admitted to Stable. Body-only enrollment never grants checked theorem use.