Horner traces · totality · uniqueness · Constructive arithmetic

Constructive polynomial evaluation

Horner(b,c,x,ℓ,z) · zᵢ₊₁ = zᵢx + aᵢ

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

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

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 441 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 PH0002 and follow only the lemmas and conservative definitions supporting beta_horner_eval_exists.

Trace prerequisites →
Zoom between mathematical scales: complete research atlas → research domain → proof family → T12 milestone → theorem and definition dependencies.
Major independently established statements: PH0005 beta_horner_eval_exists_unique · PH0007 beta_horner_eval_successor_decompose · PH0002 beta_horner_eval_exists.
Independently verified Alpha v34 checked-use theorem family: 7 dependency-curried kernel-checked theorem bodies · 25 proof prerequisites · 3 linked definitions · 2 definition-dependency arrows · 441 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.