Actual division executions · formal coefficient equivalence · Constructive arithmetic

Prime-Field Polynomial Euclidean Division

Prime(p) ∧ BetaPrefixInto(ab,ac,L,p) ∧ FpRepresentedDegree(p,bb,bc,S d,d) ⇒ ∃qb qc q rb rc R. FpPolynomialDivisionExecution(p,ab,ac,L,bb,bc,d,qb,qc,q,rb,rc,R)

Construct quotient and remainder executions over prime fields, prove their formal identity and degree bounds, and transport arithmetic across different highest-degree-first representations.

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

Open the exact edition →

Focused route

Final dependency cone

Start at theorem PX0079 and follow only the lemmas and conservative definitions supporting prime_field_polynomial_convolution_equivalent_congruent.

Trace prerequisites →
Zoom between mathematical scales: complete research atlas → research domain → proof family → G091 milestone → theorem and definition dependencies.
Major independently established statements: PX0059 prime_field_polynomial_division_execution_functional · PX005A prime_field_polynomial_division_execution_exists_unique · PX0070 prime_field_polynomial_convolution_both_left_paddings_equivalent · PX0071 prime_field_polynomial_convolution_both_left_paddings_exists · PX0072 prime_field_polynomial_equivalent_implies_left_pad · PX0075 prime_field_polynomial_add_equivalent_congruent · PX0076 prime_field_polynomial_subtract_equivalent_congruent · PX0079 prime_field_polynomial_convolution_equivalent_congruent.
Independently verified Alpha v34 checked-use theorem family: 121 dependency-curried kernel-checked theorem bodies · 461 proof prerequisites · 35 linked definitions · 71 definition-dependency arrows · 9068 exact tactic lines · first admitted v33 · not Stable. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 377 bundle nodes; SHA-256 6ae667d8518e4dbe722bb08ad1b08715a0d282c2893e533c8133d770fe861dcf.
Exact mathematical boundary: Coefficients are highest-degree-first. The divisor has a nonzero decoded head; primality supplies its actual inverse. Empty quotients and remainders are included. Functionality compares the constructed execution lengths and decoded coefficients, never arbitrary beta codes. Formal polynomial equivalence compares every coefficient, not evaluations on a finite field. The formal identity and remainder-degree bound are proved separately, not assumed by the execution graph. Arbitrary quotient/remainder-pair uniqueness from a formal identity, multiplication associativity, gcd/Bezout, irreducible-polynomial existence, and the full G091 prime-power-field goal remain open. The seven displayed new names are conservative first-order notation, not new kernel primitives.