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

Prime-field coefficient tables and Horner evaluation

Public research checkpoint, not admitted to Alpha or Stable. Alpha v30 remains 3222 checked-use theorems; Stable remains 432. The on-demand Alpha Lean service does not yet expose these checkpoint theorems; their independently checked literal bundles and unchanged sources are available below.

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

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: research checkpoint map → 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.
Public research checkpoint, independently verified: 49 theorems in a complete dependency-closed HA bundle · 131 proof prerequisites · 21 linked definitions · 36 definition-dependency arrows · 2829 exact tactic lines. Not Alpha-enrolled; no Alpha checked-use authority; not Stable. Alpha v30 remains 3222 theorems and Stable remains 432. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 202 bundle nodes; SHA-256 6e3a08c73b8a45de127e6d50a771f95b52fd54894b1c2e43468751421488a01a. Inspect the checkpoint receipt, literal bundle, and source files →
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.