CF0001 continued_fraction_initial_state_existsEvery natural initializes an actual beta-coded terminal Euclidean state (a,0,nil).
Alpha v34 checked-use · first admitted v20 · independently kernel and Lean verified; not StableCurrent 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.
CF0002 continued_fraction_empty_traceThe zero-divisor Euclidean base case has exactly the empty quotient list and no transitions.
Alpha v34 checked-use · first admitted v20 · independently kernel and Lean verified; not StableCF0003 continued_fraction_empty_trace_existsFor every dividend, a fully witnessed empty reverse Euclidean history exists at divisor zero.
Alpha v34 checked-use · first admitted v20 · independently kernel and Lean verified; not StableCF0004 continued_fraction_trace_extendA strict Euclidean division prepends its quotient and extends one beta-coded history without changing any earlier state.
Alpha v34 checked-use · first admitted v20 · independently kernel and Lean verified; not StableCF0005 continued_fraction_trace_exists_up_toBounded natural induction terminates Euclid at zero and builds a complete forward quotient list for every divisor below its bound.
Alpha v34 checked-use · first admitted v20 · independently kernel and Lean verified; not StableCF0006 continued_fraction_trace_existsEvery pair of natural numbers, including zero-input boundaries, has a finite completely witnessed Euclidean quotient trace.
Alpha v34 checked-use · first admitted v20 · independently kernel and Lean verified; not StableCF0007 continued_fraction_nonzero_divisor_existsEvery nonzero divisor produces a strictly positive trace length and a genuinely nonempty forward quotient list.
Alpha v34 checked-use · first admitted v20 · independently kernel and Lean verified; not StableCF0008 continued_fraction_positive_nonempty_existsEvery positive rational input has a complete simple continued fraction whose exact cell-coded quotient list is nonempty.
Alpha v34 checked-use · first admitted v20 · independently kernel and Lean verified; not StableCF0009 continued_fraction_positive_existsG071: every pair of strictly positive naturals admits its complete witnessed finite simple continued-fraction quotient list.
Alpha v34 checked-use · first admitted v20 · independently kernel and Lean verified; not StableND0001 Beta(b,c,i,x)Exact hygienic Gödel-beta extraction; a signature-identical alias of checked BetaAt.
Conservative definition · notation layer 0PD0002 Lt(a,b)Witness-defined strict order on natural numbers.
Conservative definition · notation layer 0ND0009 ListCell(s,q,t)The exact tagged natural-number list cell containing quotient q and tail t.
Conservative definition · notation layer 0ND0010 ContinuedFractionTrace(a,b,s,u,v,ell)A finite beta-coded reverse Euclidean history whose quotient list has forward continued-fraction order.
Conservative definition · notation layer 1ND0011 ContinuedFraction(a,b,s)Positive natural inputs together with a witnessed nonempty complete simple continued fraction.
Conservative definition · notation layer 2Only proof arrows are theorem dependencies. Definition arrows are hygienic abbreviations of exact first-order formulas and introduce no axiom or kernel symbol.