Constructive polynomial evaluation — Exact Proof Explorer

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

7 theorem bodies · 25 proof edges · 441 tactic lines · 3 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.

7 theorems
012
PH0001 · beta_prefix_horner_trace_exists

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

layer 0 · 137 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable
PH0002 · beta_horner_eval_exists

Every coded natural polynomial has an actual witnessed Horner evaluation.

layer 1 · 27 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable
PH0003 · beta_horner_trace_functional

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

layer 0 · 160 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable
PH0004 · beta_horner_eval_functional

The beta-coded polynomial-evaluation relation is functional.

layer 1 · 25 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable
PH0005 · beta_horner_eval_exists_unique

Every coded natural polynomial has exactly one witnessed evaluation.

layer 2 · 23 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable
PH0006 · beta_horner_eval_empty

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

layer 0 · 17 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable
PH0007 · beta_horner_eval_successor_decompose

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

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

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