theorem Hex.FpPoly.instDivModLawsZMod64_2 {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] : DensePoly.DivModLaws (ZMod64 p)

theorem Hex.FpPoly.Quotient.eval_reduce_eq_reduce_composeModMonic {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {g : FpPoly p} {hmonic : DensePoly.Monic g} {hg_pos : 0 < DensePoly.natDegree g} (f b : FpPoly p) : eval f (reduce b) = reduce (f.composeModMonic b g hmonic)

Modular composition on representatives is evaluation in the quotient.

This is the bridge a computed fact has to cross to become a statement about field elements: composeModMonic f b g = 0 is decide-able, and says exactly that f vanishes at the class of b.

theorem Hex.FpPoly.Quotient.eval_reduce_eq_reduce_composeModMonicImpl {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {g : FpPoly p} {hmonic : DensePoly.Monic g} {hg_pos : 0 < DensePoly.natDegree g} (f b : FpPoly p) : eval f (reduce b) = reduce (f.composeModMonicImpl b g hmonic)

The composeModMonicImpl spelling of Hex.FpPoly.Quotient.eval_reduce_eq_reduce_composeModMonic, for callers whose computation ran through the compiled Horner loop.

theorem Hex.FpPoly.Quotient.Internal.eval_X_eq_reduce {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {g : FpPoly p} {hmonic : DensePoly.Monic g} {hg_pos : 0 < DensePoly.natDegree g} (f : FpPoly p) : eval f X = reduce f

Evaluating a polynomial at the quotient class of X returns its quotient class.

This is the quotient evaluation map's defining property, stated for the project-side evaluator and executable reduction used by Conway compatibility.

theorem Hex.FpPoly.Quotient.eval_reduce_eq_zero_of_composeModMonicImpl_eq_zero {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {g : FpPoly p} {hmonic : DensePoly.Monic g} {hg_pos : 0 < DensePoly.natDegree g} {f b : FpPoly p} (h : f.composeModMonicImpl b g hmonic = 0) : eval f (reduce b) = 0

A vanishing modular composition says the polynomial has the class of b as a root.

The decide-able left-hand side and the field-level right-hand side, in one step.