def Hex.ZPoly.coeffwiseDiv (f : ZPoly) (m : Nat) : ZPoly

Divide every coefficient by m using Lean's truncating integer division.

Equations

• f.coeffwiseDiv m = Hex.DensePoly.ofList (List.map (fun (i : Nat) => Hex.DensePoly.coeff f i / Int.ofNat m) (List.range (Hex.DensePoly.size f)))

@[simp]

theorem Hex.ZPoly.coeff_coeffwiseDiv (f : ZPoly) (m i : Nat) : DensePoly.coeff (f.coeffwiseDiv m) i = DensePoly.coeff f i / Int.ofNat m

The i-th coefficient of coeffwiseDiv f m is the truncating integer quotient of f.coeff i by m. Lets a caller rewrite coefficient queries on the divided polynomial straight back to a division on the original coefficient, with no dependence on the polynomial's size.

structure Hex.LinearLiftResult : Type

Result of one linear Hensel lift step, packaging the lifted first factor g and the lifted complementary factor h. Callers can pattern-match on the two projections directly; the forward theorems linearHenselStep_g and linearHenselStep_h provide simplifying equations for them.

• g : ZPoly

  The lifted first factor.

• h : ZPoly

  The lifted complementary factor.

def Hex.LinearLiftResult.liftScaledIncrement (p k : Nat) [ZMod64.Bounds p] (r : FpPoly p) : ZPoly

The lifted-and-scaled increment used by one linear Hensel step.

Equations

• Hex.LinearLiftResult.liftScaledIncrement p k r = Hex.DensePoly.scale (Int.ofNat (p ^ k)) r.liftToZ

@[simp]

theorem Hex.LinearLiftResult.coeff_liftScaledIncrement (p k : Nat) [ZMod64.Bounds p] (r : FpPoly p) (i : Nat) : DensePoly.coeff (liftScaledIncrement p k r) i = Int.ofNat (p ^ k) * Int.ofNat (DensePoly.coeff r i).toNat

The i-th coefficient of liftScaledIncrement p k r is p ^ k times the nonnegative lift of r.coeff i. Exposes the increment added during a linear Hensel step coefficientwise, so a caller can track exactly how much each coefficient moves and confirm the change is a multiple of the current modulus p ^ k.

theorem Hex.LinearLiftResult.congr_liftScaledIncrement_zero (p k : Nat) [ZMod64.Bounds p] (r : FpPoly p) : (liftScaledIncrement p k r).congr 0 (p ^ k)

A scaled lift is coefficientwise zero modulo the scaling modulus.

def Hex.ZPoly.linearHenselStep (p k : Nat) [ZMod64.Bounds p] (f g h : ZPoly) (s t : FpPoly p) : LinearLiftResult

One linear Hensel correction step from modulus p^k to p^(k+1).

Equations

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

@[simp]

theorem Hex.ZPoly.linearHenselStep_g (p k : Nat) [ZMod64.Bounds p] (f g h : ZPoly) (s t : FpPoly p) : (linearHenselStep p k f g h s t).g = have e := (f - g * h).coeffwiseDiv (p ^ k); have gMod := modP p g; have eMod := modP p e; have qr := DensePoly.divMod (t * eMod) gMod; (g + LinearLiftResult.liftScaledIncrement p k qr.snd).reduceModPow p (k + 1)

The g projection of a linear Hensel step, exposed without unfolding the result record.

@[simp]

theorem Hex.ZPoly.linearHenselStep_h (p k : Nat) [ZMod64.Bounds p] (f g h : ZPoly) (s t : FpPoly p) : (linearHenselStep p k f g h s t).h = have e := (f - g * h).coeffwiseDiv (p ^ k); have gMod := modP p g; have hMod := modP p h; have eMod := modP p e; have qr := DensePoly.divMod (t * eMod) gMod; have hCorrection := s * eMod + qr.fst * hMod; (h + LinearLiftResult.liftScaledIncrement p k hCorrection).reduceModPow p (k + 1)

The h projection of a linear Hensel step, exposed without unfolding the result record.

theorem Hex.ZPoly.linearHenselStep_g_congr_mod_base (p k : Nat) [ZMod64.Bounds p] (f g h : ZPoly) (s t : FpPoly p) (hk : 1 ≤ k) : (linearHenselStep p k f g h s t).g.congr g p

One linear Hensel step changes the leading factor g only by a multiple of the current modulus, so the stepped factor is congruent to g modulo the base prime p (for 1 ≤ k).

theorem Hex.ZPoly.linearHenselStep_h_congr_mod_base (p k : Nat) [ZMod64.Bounds p] (f g h : ZPoly) (s t : FpPoly p) (hk : 1 ≤ k) : (linearHenselStep p k f g h s t).h.congr h p

One linear Hensel step changes the cofactor h only by a multiple of the current modulus, so the stepped cofactor is congruent to h modulo the base prime p (for 1 ≤ k).

theorem Hex.ZPoly.congr_liftToZ_of_modP_eq (p : Nat) [ZMod64.Bounds p] (u : FpPoly p) (z : ZPoly) (h : modP p z = u) : u.liftToZ.congr z p

A modP p equality converts to a ZPoly.congr against the lift: if modP p z = u then the lifted-back-to-ZPoly representative FpPoly.liftToZ u agrees with z coefficientwise modulo p. Used by the correction-proof chain when an FpPoly-side computation has produced the canonical residue and the caller needs to feed it back into the integer-side congruence.

theorem Hex.ZPoly.liftToZ_add_congr (p : Nat) [ZMod64.Bounds p] (f g : FpPoly p) : (f + g).liftToZ.congr (f.liftToZ + g.liftToZ) p

FpPoly.liftToZ is additive modulo p: the integer lift of a sum is coefficientwise congruent to the sum of the integer lifts. Together with liftToZ_mul_congr this is the congruence used by modP_add / modP_lift_mul_left / modP_lift_mul_right to push modP p through the +/· structure of the linear Hensel correction.

theorem Hex.ZPoly.liftToZ_mul_congr (p : Nat) [ZMod64.Bounds p] (f g : FpPoly p) : (f * g).liftToZ.congr (f.liftToZ * g.liftToZ) p

FpPoly.liftToZ is multiplicative modulo p: the integer lift of a product is coefficientwise congruent to the product of the integer lifts. Multiplicative companion of liftToZ_add_congr; together they translate the FpPoly-side ring operations into ZPoly.congr form, which the modP push lemmas (modP_add, modP_lift_mul_left, modP_lift_mul_right) consume to expose the linear Hensel correction's mod-p structure.

@[simp]

theorem Hex.ZPoly.modP_add (p : Nat) [ZMod64.Bounds p] (f g : ZPoly) : modP p (f + g) = modP p f + modP p g

ZPoly.modP p distributes over addition: the canonical mod-p residue of a sum is the sum of residues. Standard ring-homomorphism rewrite for modP p used by the linear Hensel step proof to split modP p (g·h + ...) into manageable pieces.

@[simp]

theorem Hex.ZPoly.modP_mul (p : Nat) [ZMod64.Bounds p] (f g : ZPoly) : modP p (f * g) = modP p f * modP p g

ZPoly.modP p distributes over multiplication: the canonical mod-p residue of a product is the product of residues. Multiplicative companion of modP_add; the Mathlib-free Gauss-transfer chain consumes this to expose modP p (f * g) in its factored form.

theorem Hex.ZPoly.modP_lift_mul_left (p : Nat) [ZMod64.Bounds p] (r : FpPoly p) (h : ZPoly) : modP p (r.liftToZ * h) = r * modP p h

modP p reduces a liftToZ-on-the-left product to the FpPoly-side factor times the modP of the integer side: modP p (liftToZ r · h) = r · modP p h. Companion of modP_lift_mul_right; consumed by the linear Hensel step's correctness chain to push modP p past the s * eMod-shaped half of the correction product.

theorem Hex.ZPoly.modP_lift_mul_right (p : Nat) [ZMod64.Bounds p] (g : ZPoly) (hCorrection : FpPoly p) : modP p (g * hCorrection.liftToZ) = modP p g * hCorrection

modP p reduces a liftToZ-on-the-right product to the modP of the integer side times the FpPoly-side factor: modP p (g · liftToZ hCorrection) = modP p g · hCorrection. Companion of modP_lift_mul_left; consumed by the linear Hensel step's correctness chain to push modP p past the q * hMod-shaped half of the correction product.

theorem Hex.ZPoly.modP_add_lift_mul (p : Nat) [ZMod64.Bounds p] (g h : ZPoly) (r hCorrection : FpPoly p) : modP p (r.liftToZ * h + g * hCorrection.liftToZ) = r * modP p h + modP p g * hCorrection

Combined modP_add + modP_lift_mul_left + modP_lift_mul_right rewrite in the exact liftToZ r · h + g · liftToZ hCorrection shape produced by the linear Hensel correction step. Single-rewrite entry point consumed by the linear-Hensel correctness chain in place of three separate modP pushes.

def Hex.ZPoly.LinearLiftLoopInvariant (p current : Nat) [ZMod64.Bounds p] (f : ZPoly) (s t : FpPoly p) (acc : LinearLiftResult) : Prop

The proof state carried by the linear Hensel loop at precision p^current.

The final 0 < acc.g.natDegree component records that the lifted leading factor is nonconstant. It propagates trivially through the loop (the linear step preserves acc.g's degree) and is exactly what makes the per-step degree obligation LinearLiftStepDegreeInvariant provable from the invariant alone: without it the admissible constant case acc.g = 1 satisfies every other component yet has degree 0, so no strict degree drop is available.

Equations

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

@[simp]

theorem Hex.ZPoly.LinearLiftLoopInvariant.product_congr {p current : Nat} [ZMod64.Bounds p] {f : ZPoly} {s t : FpPoly p} {acc : LinearLiftResult} (hinv : LinearLiftLoopInvariant p current f s t acc) : (acc.g * acc.h).congr f (p ^ current)

The product-congruence component of a linear-lift loop invariant.

@[simp]

theorem Hex.ZPoly.LinearLiftLoopInvariant.bezout_congr {p current : Nat} [ZMod64.Bounds p] {f : ZPoly} {s t : FpPoly p} {acc : LinearLiftResult} (hinv : LinearLiftLoopInvariant p current f s t acc) : (s * modP p acc.g + t * modP p acc.h).liftToZ.congr 1 p

The Bezout-congruence component of a linear-lift loop invariant.

@[simp]

theorem Hex.ZPoly.LinearLiftLoopInvariant.monic_g {p current : Nat} [ZMod64.Bounds p] {f : ZPoly} {s t : FpPoly p} {acc : LinearLiftResult} (hinv : LinearLiftLoopInvariant p current f s t acc) : DensePoly.Monic acc.g

The monicity component of a linear-lift loop invariant.

@[simp]

theorem Hex.ZPoly.LinearLiftLoopInvariant.pos_degree {p current : Nat} [ZMod64.Bounds p] {f : ZPoly} {s t : FpPoly p} {acc : LinearLiftResult} (hinv : LinearLiftLoopInvariant p current f s t acc) : 0 < DensePoly.natDegree acc.g

The positive-degree (nonconstant) component of a linear-lift loop invariant.

def Hex.ZPoly.LinearLiftStepDegreeInvariant (p current : Nat) [ZMod64.Bounds p] (f : ZPoly) (_s t : FpPoly p) (acc : LinearLiftResult) : Prop

The per-step degree hypothesis needed to preserve monicity of the g factor.

Equations

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

def Hex.ZPoly.henselLift (p k : Nat) [ZMod64.Bounds p] (f g h : ZPoly) (s t : FpPoly p) : LinearLiftResult

Lift a factorization modulo p to a factorization modulo p^k by iterating the linear Hensel step.

Equations

• Hex.ZPoly.henselLift p 0 f g h s t = { g := g.reduceModPow p 0, h := h.reduceModPow p 0 }
• Hex.ZPoly.henselLift p steps_1.succ f g h s t = Hex.ZPoly.henselLiftLoop✝ p steps_1 1 f s t { g := g.reduceModPow p 1, h := h.reduceModPow p 1 }

theorem Hex.ZPoly.linearHenselStep_spec (p k : Nat) [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f g h : ZPoly) (s t : FpPoly p) (hk : 1 ≤ k) (hprod : (g * h).congr f (p ^ k)) (hbez : (s * modP p g + t * modP p h).liftToZ.congr 1 p) (hmonic : DensePoly.Monic g) : have r := linearHenselStep p k f g h s t; (r.g * r.h).congr f (p ^ (k + 1))

The lifted factors still multiply to f modulo the next power of p.

theorem Hex.ZPoly.reduceModPow_monic_of_monic (p k : Nat) (f : ZPoly) (hp : 1 < p) (hmonic : DensePoly.Monic f) : DensePoly.Monic (f.reduceModPow p (k + 1))

Reducing a monic ZPoly modulo p ^ (k + 1) keeps it monic, provided 1 < p. The hypothesis guarantees the modulus exceeds the leading coefficient 1, so reduction leaves it fixed and does not raise the degree; callers rely on this to know the lifted factors stay monic across every linear Hensel step.

theorem Hex.ZPoly.linearHenselStep_monic (p k : Nat) [ZMod64.Bounds p] (f g h : ZPoly) (s t : FpPoly p) (hp : 1 < p) (hmonic : DensePoly.Monic g) (hgCorrectionDegree : have e := (f - g * h).coeffwiseDiv (p ^ k); have gMod := modP p g; have eMod := modP p e; have qr := DensePoly.divMod (t * eMod) gMod; DensePoly.natDegree (LinearLiftResult.liftScaledIncrement p k qr.snd) < DensePoly.natDegree g) : DensePoly.Monic (linearHenselStep p k f g h s t).g

The linear step preserves monicity of the lifted g factor.

theorem Hex.ZPoly.linearHenselStep_g_degree?_eq (p k : Nat) [ZMod64.Bounds p] (f g h : ZPoly) (s t : FpPoly p) (hp : 1 < p) (hmonic : DensePoly.Monic g) (hgCorrectionDegree : have e := (f - g * h).coeffwiseDiv (p ^ k); have gMod := modP p g; have eMod := modP p e; have qr := DensePoly.divMod (t * eMod) gMod; DensePoly.natDegree (LinearLiftResult.liftScaledIncrement p k qr.snd) < DensePoly.natDegree g) : DensePoly.degree? (linearHenselStep p k f g h s t).g = DensePoly.degree? g

The linear step preserves the degree of the monic g factor.

theorem Hex.ZPoly.henselLift_spec (p k : Nat) [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f g h : ZPoly) (s t : FpPoly p) (hk : 1 ≤ k) (hp : 1 < p) (hstart : LinearLiftLoopInvariant p 1 f s t { g := g.reduceModPow p 1, h := h.reduceModPow p 1 }) (hstepDegree : ∀ (n : Nat) (state : LinearLiftResult), 1 ≤ n → LinearLiftLoopInvariant p n f s t state → LinearLiftStepDegreeInvariant p n f s t state) (hstepBezout : ∀ (n : Nat) (state : LinearLiftResult), 1 ≤ n → LinearLiftLoopInvariant p n f s t state → have next := linearHenselStep p n f state.g state.h s t; (s * modP p next.g + t * modP p next.h).liftToZ.congr 1 p) : have r := henselLift p k f g h s t; (r.g * r.h).congr f (p ^ k)

The iterative linear wrapper lifts the factorization to congruence modulo p^k.

theorem Hex.ZPoly.henselLift_monic (p k : Nat) [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f g h : ZPoly) (s t : FpPoly p) (hk : 1 ≤ k) (hp : 1 < p) (hstart : LinearLiftLoopInvariant p 1 f s t { g := g.reduceModPow p 1, h := h.reduceModPow p 1 }) (hstepDegree : ∀ (n : Nat) (state : LinearLiftResult), 1 ≤ n → LinearLiftLoopInvariant p n f s t state → LinearLiftStepDegreeInvariant p n f s t state) (hstepBezout : ∀ (n : Nat) (state : LinearLiftResult), 1 ≤ n → LinearLiftLoopInvariant p n f s t state → have next := linearHenselStep p n f state.g state.h s t; (s * modP p next.g + t * modP p next.h).liftToZ.congr 1 p) : DensePoly.Monic (henselLift p k f g h s t).g

The iterative linear wrapper preserves monicity of the lifted g factor.

theorem Hex.ZPoly.henselLift_congr_of_base (p k : Nat) [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f g h : ZPoly) (s t : FpPoly p) (hk : 1 ≤ k) (hp : 1 < p) (hprod : (g * h).congr f p) (hbez : (s * modP p g + t * modP p h).liftToZ.congr 1 p) (hmonic : DensePoly.Monic g) (hgdeg : 0 < DensePoly.natDegree g) : have r := henselLift p k f g h s t; (r.g * r.h).congr f (p ^ k)

Convenience corollary of henselLift_spec: the lifted factorization is congruent to f modulo p^k, discharging the loop preconditions internally from the base mod-p factorization data plus a nonconstant hypothesis on g. The nonconstant condition 0 < g.natDegree is genuine; it is what makes the per-step degree drop available; the admissible constant case g = 1 has no such drop.

theorem Hex.ZPoly.henselLift_monic_of_base (p k : Nat) [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f g h : ZPoly) (s t : FpPoly p) (hk : 1 ≤ k) (hp : 1 < p) (hprod : (g * h).congr f p) (hbez : (s * modP p g + t * modP p h).liftToZ.congr 1 p) (hmonic : DensePoly.Monic g) (hgdeg : 0 < DensePoly.natDegree g) : DensePoly.Monic (henselLift p k f g h s t).g

Convenience corollary of henselLift_monic: the lifted leading factor stays monic, discharging the loop preconditions internally from the base mod-p factorization data plus the nonconstant hypothesis on g.

theorem Hex.ZPoly.henselLift_degree?_of_base (p k : Nat) [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f g h : ZPoly) (s t : FpPoly p) (hk : 1 ≤ k) (hp : 1 < p) (hprod : (g * h).congr f p) (hbez : (s * modP p g + t * modP p h).liftToZ.congr 1 p) (hmonic : DensePoly.Monic g) (hgdeg : 0 < DensePoly.natDegree g) : DensePoly.degree? (henselLift p k f g h s t).g = DensePoly.degree? g

Convenience corollary of the linear Hensel loop invariants: the lifted leading factor has the same executable degree as the base g.

theorem Hex.ZPoly.henselLift_g_congr_mod_base (p k : Nat) [ZMod64.Bounds p] (f g h : ZPoly) (s t : FpPoly p) (hk : 1 ≤ k) : (henselLift p k f g h s t).g.congr g p

The iterative linear wrapper changes the leading factor only by multiples of the modulus, so the lifted factor is congruent to the input g modulo the base prime p. Companion to henselLift_spec; the linear-loop analogue of henselLiftQuadratic_g_congr_mod_base.

theorem Hex.ZPoly.henselLift_h_congr_mod_base (p k : Nat) [ZMod64.Bounds p] (f g h : ZPoly) (s t : FpPoly p) (hk : 1 ≤ k) : (henselLift p k f g h s t).h.congr h p

The iterative linear wrapper changes the cofactor only by multiples of the modulus, so the lifted cofactor is congruent to the input h modulo the base prime p. Companion to henselLift_spec; the linear-loop analogue of henselLiftQuadratic_h_congr_mod_base.