Exact Horner derivatives · constructive traces · G095 partial · Constructive arithmetic

Formal polynomial differentiation and Hensel foundations

∀b,c,t,ℓ. ∃!n,z. HornerDerivative(b,c,t,ℓ,n,z)

Independently checked constructive theorems build coupled beta-coded Horner value and formal-derivative traces for arbitrary natural polynomials, including exact successor laws and uniqueness.

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

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 583 native tactic lines and 27 actual proof prerequisites with every definition fully expanded.

Open the exact edition →

Focused route

Final dependency cone

Start at theorem HD000B and follow only the lemmas and conservative definitions supporting beta_horner_derivative_exists_unique.

Trace prerequisites →
Zoom between mathematical scales: complete research atlas → research domain → proof family → G095 milestone → theorem and definition dependencies.
Major independently established statements: HD0002 beta_horner_derivative_value_exists · HD0008 beta_horner_derivative_successor_decompose · HD0009 beta_horner_derivative_functional · HD000D beta_horner_derivative_only_exists_unique · HD000B beta_horner_derivative_exists_unique.
Independently verified Alpha v34 checked-use theorem family: 15 dependency-curried kernel-checked theorem bodies · 27 proof prerequisites · 12 linked definitions · 13 definition-dependency arrows · 583 exact tactic lines · first admitted v24 · not Stable. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 203 bundle nodes; SHA-256 627e39ed29b10db48bf37d5bef8750d48009a7524c822a7c5e7c83e96a8e9cf9.
Exact mathematical boundary: Historical partial components only: this chapter proves arbitrary natural polynomial values and unique formal derivatives. G095 is now closed in the separate Alpha-v27 hensel-lifting branch for integer polynomials, unrestricted input roots, unique canonical lifts, and every positive prime power.

Separate complete second-wave branches: Full G095 proof · Alpha v27.