structure Hex.QuadraticLiftResult : Type

Output of one quadratic Hensel doubling step. The four fields package the updated leading factor g (monic, the input g corrected modulo m^2), the updated complementary factor h, and the updated Bezout witnesses s, t satisfying s * g + t * h ≡ 1 (mod m^2).

• g : ZPoly

  The updated monic factor.

• h : ZPoly

  The updated complementary factor.

• s : ZPoly

  The updated Bezout coefficient multiplying g.

• t : ZPoly

  The updated Bezout coefficient multiplying h.

def Hex.QuadraticLiftResult.reduceModSquare (f : ZPoly) (m : Nat) : ZPoly

Canonical coefficient reduction modulo m^2.

Equations

• Hex.QuadraticLiftResult.reduceModSquare f m = f.reduceModPow m 2

def Hex.QuadraticLiftResult.factorError (f g h : ZPoly) : ZPoly

Residue f - g * h corrected by the factor update of the quadratic Hensel step: starting from g * h ≡ f (mod m), this quantity is divisible by m and its lift drives the first-order correction that achieves g' * h' ≡ f (mod m^2).

Equations

• Hex.QuadraticLiftResult.factorError f g h = f - g * h

def Hex.QuadraticLiftResult.factorErrorImpl (f g h : ZPoly) : ZPoly

Runtime implementation of factorError: the same residual with the product taken by Kronecker substitution (Hex.ZPoly.mulKronecker, value-equal to the schoolbook product by Hex.ZPoly.mulKronecker_eq). The bignum Hensel step is the only caller, and its g * h is the widest product in the lift.

Equations

• Hex.QuadraticLiftResult.factorErrorImpl f g h = f - g.mulKronecker h

@[csimp]

theorem Hex.QuadraticLiftResult.factorError_eq_impl : factorError = factorErrorImpl

Register the Kronecker product as the compiled implementation of factorError.

def Hex.ZPoly.quadraticModulus (m : Nat) : Nat

The working modulus m * m = m² of one quadratic Hensel doubling step.

Equations

• Hex.ZPoly.quadraticModulus m = m * m

def Hex.ZPoly.canonicalMod (z : Int) (modulus : Nat) : Int

Canonical nonnegative residue of z in the range [0, modulus).

Equations

• Hex.ZPoly.canonicalMod z modulus = Int.ofNat (z % Int.ofNat modulus).toNat

def Hex.ZPoly.reduceCoeffModSquare (z : Int) (m : Nat) : Int

Reduce a single coefficient to its canonical residue modulo m².

Equations

• Hex.ZPoly.reduceCoeffModSquare z m = Hex.ZPoly.canonicalMod z (Hex.ZPoly.quadraticModulus m)

def Hex.ZPoly.addModSquare (f g : ZPoly) (m : Nat) : ZPoly

Polynomial sum f + g with every coefficient reduced modulo m².

Equations

• f.addModSquare g m = Hex.QuadraticLiftResult.reduceModSquare (f + g) m

def Hex.ZPoly.subModSquare (f g : ZPoly) (m : Nat) : ZPoly

Polynomial difference f - g with every coefficient reduced modulo m².

Equations

• f.subModSquare g m = Hex.QuadraticLiftResult.reduceModSquare (f - g) m

def Hex.ZPoly.mulModSquare (f g : ZPoly) (m : Nat) : ZPoly

Polynomial product f * g with every coefficient reduced modulo m².

Public, unlike its sibling reductions, because its compiled implementation is swapped by a @[csimp] theorem, and csimp lemmas must be public.

Equations

• f.mulModSquare g m = Hex.QuadraticLiftResult.reduceModSquare (f * g) m

def Hex.ZPoly.mulModSquareImpl (f g : ZPoly) (m : Nat) : ZPoly

Runtime implementation of mulModSquare: the same reduced product with the multiplication taken by Kronecker substitution. Eight of the nine polynomial products in the bignum quadratic step go through this definition.

Equations

• f.mulModSquareImpl g m = Hex.QuadraticLiftResult.reduceModSquare (f.mulKronecker g) m

@[csimp]

theorem Hex.ZPoly.mulModSquare_eq_impl : mulModSquare = mulModSquareImpl

Register the Kronecker product as the compiled implementation of mulModSquare.

def Hex.ZPoly.mulMonomialModSquare (k : Nat) (coeff : Int) (q : ZPoly) (m : Nat) : ZPoly

Modular multiplication by a single monomial. Kept as a separate specification so compiled division can avoid sending the monomial's leading zero coefficients through the generic schoolbook multiplier.

Equations

• Hex.ZPoly.mulMonomialModSquare k coeff q m = Hex.ZPoly.mulModSquare (Hex.DensePoly.monomial k coeff) q m

def Hex.ZPoly.mulMonomialModSquareImpl (k : Nat) (coeff : Int) (q : ZPoly) (m : Nat) : ZPoly

Linear-time implementation of modular monomial multiplication.

Equations

• Hex.ZPoly.mulMonomialModSquareImpl k coeff q m = Hex.QuadraticLiftResult.reduceModSquare (Hex.DensePoly.shift k (Hex.DensePoly.scale coeff q)) m

theorem Hex.ZPoly.mulMonomialModSquare_eq (k : Nat) (coeff : Int) (q : ZPoly) (m : Nat) : mulMonomialModSquare k coeff q m = mulMonomialModSquareImpl k coeff q m

The shift-and-scale monomial kernel is exactly the generic modular product.

@[csimp]

theorem Hex.ZPoly.mulMonomialModSquare_eq_impl : mulMonomialModSquare = mulMonomialModSquareImpl

Proof-backed compiled implementation of modular monomial multiplication.

def Hex.ZPoly.divModMonicModSquareAux (m : Nat) (q : ZPoly) : Nat → ZPoly → ZPoly → ZPoly × ZPoly

Fuel-driven long-division kernel returning the quotient/remainder of the running rem by the monic divisor q, with all arithmetic reduced modulo m². The Hensel theorem surface supplies monic divisors, so this exploits that invariant to avoid coefficient division in the modular hot path.

Equations

• One or more equations did not get rendered due to their size.
• Hex.ZPoly.divModMonicModSquareAux m q 0 x✝¹ x✝ = (x✝¹, x✝)

def Hex.ZPoly.divModMonicModSquare (p q : ZPoly) (m : Nat) : ZPoly × ZPoly

Quotient and remainder of p divided by the monic divisor q, working modulo m², with the dividend size supplying the recursion fuel.

Public, unlike its Aux worker, because its compiled implementation is swapped by a @[csimp] theorem, and csimp lemmas must be public.

Equations

• p.divModMonicModSquare q m = Hex.ZPoly.divModMonicModSquareAux m q (Hex.DensePoly.size (Hex.QuadraticLiftResult.reduceModSquare p m)) 0 (Hex.QuadraticLiftResult.reduceModSquare p m)

def Hex.ZPoly.divModMonicModSquareImpl (p q : ZPoly) (m : Nat) : ZPoly × ZPoly

Windowed implementation of the modular monic division.

The windowed loop needs a monic divisor at a positive modulus -- the only shape the Hensel step ever divides by; every other input falls back to the specification loop, so the two agree on every input.

Equations

• One or more equations did not get rendered due to their size.

@[csimp]

theorem Hex.ZPoly.divModMonicModSquare_eq_impl : divModMonicModSquare = divModMonicModSquareImpl

Proof-backed compiled implementation of the modular monic division.