Canonical coefficients · witnessed modular histories · re-encoding · Constructive arithmetic

Prime-field coefficient tables and Horner evaluation

h₀=0; hᵢ₊₁ = hᵢ·x + aᵢ in Fₚ; coefficients are highest-degree-first

Normalize finite coefficient data, construct coefficientwise arithmetic, and execute an actual modular Horner trace using the already proved canonical field operations.

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

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 certificate

Fully expanded arithmetic

Inspect all 2829 native tactic lines and 131 actual proof prerequisites with every definition fully expanded.

Open the exact edition →

Focused route

Final dependency cone

Start at theorem PP0031 and follow only the lemmas and conservative definitions supporting prime_field_polynomial_reduce_and_evaluate_exists.

Trace prerequisites →
Zoom between mathematical scales: complete research atlas → research domain → proof family → G091 milestone → theorem and definition dependencies.
Major independently established statements: PP002A prime_field_polynomial_horner_exists_unique · PP002F prime_field_polynomial_normalized_horner_iff · PP0031 prime_field_polynomial_reduce_and_evaluate_exists.
Independently verified Alpha v34 checked-use theorem family: 49 dependency-curried kernel-checked theorem bodies · 131 proof prerequisites · 21 linked definitions · 36 definition-dependency arrows · 2829 exact tactic lines · first admitted v31 · not Stable. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 202 bundle nodes; SHA-256 6e3a08c73b8a45de127e6d50a771f95b52fd54894b1c2e43468751421488a01a.
Exact mathematical boundary: Length is representation length, not polynomial degree. Leading zeros and the empty zero polynomial are allowed; the canonical argument guard x<p also applies to the empty case. Evaluation is defined by actual field-operation steps, not an assumed residue invariant. Polynomial division, gcd, irreducibles and general prime-power extension fields remain open; this does not close G091.