Canonical coefficients · leading-zero trimming · monic and synthetic normalization · Constructive arithmetic

Polynomial division prerequisites

Prime(p) ∧ BetaPrefixInto(b,c,S n,p) ∧ Lt(a,p) ⇒ ∃qb qc r. FpSyntheticDivision(p,b,c,a,n,qb,qc,r)

Construct actual coefficient differences, trimmed and monic representatives, and synthetic quotient/remainder executions over prime fields.

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

Open the exact edition →

Focused route

Final dependency cone

Start at theorem PQ0055 and follow only the lemmas and conservative definitions supporting prime_field_polynomial_synthetic_zero_remainder_iff.

Trace prerequisites →
Zoom between mathematical scales: complete research atlas → research domain → proof family → G091 milestone → theorem and definition dependencies.
Major independently established statements: PQ000D prime_field_polynomial_subtract_exists · PQ002D prime_field_polynomial_trim_exists_unique · PQ0043 prime_field_polynomial_monic_normalization_exists_unique · PQ0054 prime_field_polynomial_synthetic_exists_unique · PQ0052 prime_field_polynomial_synthetic_represented_degree · PQ0055 prime_field_polynomial_synthetic_zero_remainder_iff.
Independently verified Alpha v34 checked-use theorem family: 85 dependency-curried kernel-checked theorem bodies · 190 proof prerequisites · 28 linked definitions · 50 definition-dependency arrows · 3641 exact tactic lines · first admitted v32 · not Stable. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 293 bundle nodes; SHA-256 fec8cf768ef2b94430d58d947daa0affada315bbc5160a03991dc4d2550dd0e9.
Exact mathematical boundary: All coefficients retain the established highest-degree-first order. Trimming handles empty and all-zero prefixes; monic normalization requires a nonzero leading coefficient. Synthetic division has a nonempty input of length S n and a quotient of length n, unique in decoded values. Its coefficient recurrence, actual evaluation remainder and positive-degree drop are checked. General polynomial Euclidean division, gcd/Bezout, an arbitrary-convolution factor theorem, irreducible-polynomial existence and the full G091 prime-power-field endpoint remain open. These exact theorems are first admitted to Alpha v32; Stable remains unchanged.