def Hex.ZPoly.quadraticHenselStepWord? (m : Nat) (f g h s t : ZPoly) : Option QuadraticLiftResult

Word-sized quadratic Hensel doubling step over WordMod at working modulus m*m, taken when m*m fits an odd machine word, 1 < m*m, and the divisor g is monic of positive degree. Byte-identical to quadraticHenselStepBignum under that guard; declines (none) otherwise.

Equations

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

def Hex.ZPoly.quadraticHenselStepBignum (m : Nat) (f g h s t : ZPoly) : QuadraticLiftResult

One quadratic Hensel correction step from modulus m to modulus m^2.

Inputs: the target polynomial f, the current monic factor g, the complementary factor h, and the Bezout witnesses s, t for the current factorisation. Preconditions consumed by the correctness theorems below are g monic, g * h ≡ f (mod m), and s * g + t * h ≡ 1 (mod m); the returned QuadraticLiftResult then satisfies the same conjuncts modulo m^2.

Equations

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

def Hex.ZPoly.quadraticHenselStepBignumImpl (m : Nat) (f g h s t : ZPoly) : QuadraticLiftResult

Runtime shape of the bignum quadratic step: the target is narrowed to the step's own modulus before the residual is formed.

Equations

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

@[csimp]

theorem Hex.ZPoly.quadraticHenselStepBignum_eq_impl : quadraticHenselStepBignum = quadraticHenselStepBignumImpl

Proof-backed compiled implementation of the bignum quadratic step.

def Hex.ZPoly.quadraticHenselStep (m : Nat) (f g h s t : ZPoly) : QuadraticLiftResult

Guarded selection: the word-sized step when its guard holds, else the bignum step.

Equations

• Hex.ZPoly.quadraticHenselStep m f g h s t = match Hex.ZPoly.quadraticHenselStepWord? m f g h s t with | some result => result | none => Hex.ZPoly.quadraticHenselStepBignum m f g h s t

def Hex.ZPoly.quadraticHenselFactorsBignum (m : Nat) (f g h s t : ZPoly) : ZPoly × ZPoly

Bignum factor-only quadratic step, omitting the final Bezout correction.

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

Equations

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

def Hex.ZPoly.quadraticHenselFactorsBignumImpl (m : Nat) (f g h s t : ZPoly) : ZPoly × ZPoly

Runtime shape of the bignum factor-only step, narrowing the target to the step's own modulus before the residual is formed.

Equations

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

@[csimp]

theorem Hex.ZPoly.quadraticHenselFactorsBignum_eq_impl : quadraticHenselFactorsBignum = quadraticHenselFactorsBignumImpl

Proof-backed compiled implementation of the bignum factor-only step.

def Hex.ZPoly.quadraticHenselFactors (m : Nat) (f g h s t : ZPoly) : ZPoly × ZPoly

Update only the two factors in one quadratic Hensel step. The result is byte-identical to the g and h fields of quadraticHenselStep, while the final Bezout update is skipped.

Equations

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

theorem Hex.ZPoly.quadraticHenselFactors_eq (m : Nat) (f g h s t : ZPoly) : quadraticHenselFactors m f g h s t = ((quadraticHenselStep m f g h s t).g, (quadraticHenselStep m f g h s t).h)

The factor-only step agrees exactly with the factor fields of the full quadratic step.

theorem Hex.ZPoly.quadraticHenselStepWord?_eq (m : Nat) (f g h s t : ZPoly) (h2 : m * m < UInt64.word) (hodd : UInt64.ofNat (m * m) % 2 = 1) (h1 : 1 < m * m) (hmlc : DensePoly.leadingCoeff g = 1) (hd : 0 < DensePoly.natDegree g) : quadraticHenselStepWord? m f g h s t = some (quadraticHenselStepBignum m f g h s t)

theorem Hex.ZPoly.quadraticHenselStep_eq_bignum (m : Nat) (f g h s t : ZPoly) : quadraticHenselStep m f g h s t = quadraticHenselStepBignum m f g h s t

theorem Hex.ZPoly.quadraticHenselStep_canonical (m : Nat) (f g h s t : ZPoly) (hm : 0 < m) : (quadraticHenselStep m f g h s t).g.Canonical (m * m) ∧ (quadraticHenselStep m f g h s t).h.Canonical (m * m) ∧ (quadraticHenselStep m f g h s t).s.Canonical (m * m) ∧ (quadraticHenselStep m f g h s t).t.Canonical (m * m)

Every component of one quadratic Hensel step is canonical modulo the step's working modulus m², on both the word and the bignum path.

theorem Hex.ZPoly.quadraticHenselFactors_canonical (m : Nat) (f g h s t : ZPoly) (hm : 0 < m) : (quadraticHenselFactors m f g h s t).fst.Canonical (m * m) ∧ (quadraticHenselFactors m f g h s t).snd.Canonical (m * m)

The factor-only step inherits the same coefficient-range invariant.

theorem Hex.ZPoly.quadraticHenselStep_factor_spec (m : Nat) (f g h s t : ZPoly) (hm : 0 < m) (hprod : (g * h).congr f m) (hbez : (s * g + t * h).congr 1 m) (hmonic : DensePoly.Monic g) : have r := quadraticHenselStep m f g h s t; (r.g * r.h).congr f (m * m)

The updated factors multiply to f modulo m^2.

theorem Hex.ZPoly.quadraticHenselStep_bezout_spec (m : Nat) (f g h s t : ZPoly) (hm : 1 < m) (hprod : (g * h).congr f m) (hbez : (s * g + t * h).congr 1 m) (hmonic : DensePoly.Monic g) : have r := quadraticHenselStep m f g h s t; (r.s * r.g + r.t * r.h).congr 1 (m * m)

The updated Bezout witnesses certify coprimality modulo m^2.

theorem Hex.ZPoly.quadraticHenselStep_spec (m : Nat) (f g h s t : ZPoly) (hm : 1 < m) (hprod : (g * h).congr f m) (hbez : (s * g + t * h).congr 1 m) (hmonic : DensePoly.Monic g) : have r := quadraticHenselStep m f g h s t; (r.g * r.h).congr f (m * m) ∧ (r.s * r.g + r.t * r.h).congr 1 (m * m)

The quadratic step lifts both factor and Bezout congruences to modulus m^2.

theorem Hex.ZPoly.quadraticHenselStep_monic (m : Nat) (f g h s t : ZPoly) (hm : 1 < m) (hmonic : DensePoly.Monic g) : DensePoly.Monic (quadraticHenselStep m f g h s t).g

The monic factor remains monic after the quadratic correction.

theorem Hex.ZPoly.quadraticHenselStep_factor_congr_mod_base (m : Nat) (f g h s t : ZPoly) (hm : 1 < m) (hprod : (g * h).congr f m) : (quadraticHenselStep m f g h s t).g.congr g m ∧ (quadraticHenselStep m f g h s t).h.congr h m

After a quadratic Hensel step, both the updated leading factor r.g and the updated complementary factor r.h are congruent to the corresponding input factors modulo m. The quadratic correction only touches the data modulo m^2 beyond what is already determined modulo m, so the input factorisation is preserved at the base modulus.