Horner traces · totality · uniqueness

Constructive polynomial evaluation

Seven independently checked first-order proofs construct, characterize, and uniquely evaluate every finite beta-coded natural polynomial.

7 kernel- and Lean-verified Alpha-closed theorems · 3 conservative definitions · 2 notation dependencies

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.

10 items
PH0001 beta_prefix_horner_trace_exists

Every beta-coded coefficient prefix has a complete constructive Horner trace.

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

Every coded natural polynomial has an actual witnessed Horner evaluation.

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

Any two complete Horner traces over the same polynomial have equal values.

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

The beta-coded polynomial-evaluation relation is functional.

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

Every coded natural polynomial has exactly one witnessed evaluation.

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

The empty polynomial's exact constructive Horner value is zero.

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

A nonempty polynomial splits into its evaluated prefix and final coefficient.

Alpha v34 checked-use · first admitted v20 · independently kernel and Lean verified; not Stable
ND0001 Beta(b,c,i,x)

Exact hygienic Gödel-beta extraction; a signature-identical alias of checked BetaAt.

Conservative definition · notation layer 0
PD0002 Lt(a,b)

Witness-defined strict order on natural numbers.

Conservative definition · notation layer 0
ND0002 Horner(b,c,x,ell,z)

A complete beta-coded natural-polynomial Horner trace with an explicitly witnessed terminal value.

Conservative definition · notation layer 1

Only proof arrows are theorem dependencies. Definition arrows are hygienic abbreviations of exact first-order formulas and introduce no axiom or kernel symbol.