13.5. Key correctness theorems🔗

The defining guarantee of each lifter is that the product of the lifted factors is congruent to the input modulo the target prime power. For the iterative single-split wrapper:

theorem

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

The multifactor lifters carry the same product-congruence guarantee. The proof maintains it at each node of the recursive split.

theorem

Hex.ZPoly.multifactorLift_spec (p k : ℕ) [Hex.ZMod64.Bounds p]
  [Hex.ZMod64.PrimeModulus p] (f : Hex.ZPoly)
  (factors : Array Hex.ZPoly) (hk : 1 ≤ k) (hp : 1 < p)
  (hinv : Hex.ZPoly.MultifactorLiftInvariant p k f factors.toList) :
  (Hex.ZPoly.multifactorLift p k f factors).polyProduct.congr f (p ^ k)
Hex.ZPoly.multifactorLift_spec (p k : ℕ)
  [Hex.ZMod64.Bounds p]
  [Hex.ZMod64.PrimeModulus p]
  (f : Hex.ZPoly)
  (factors : Array Hex.ZPoly) (hk : 1 ≤ k)
  (hp : 1 < p)
  (hinv :
    Hex.ZPoly.MultifactorLiftInvariant p k
      f factors.toList) :
  (Hex.ZPoly.multifactorLift p k f
          factors).polyProduct.congr
    f (p ^ k)

The product of the lifted factors is congruent to f modulo p^k, provided each recursive binary split supplies the linear Hensel invariant package.

theorem

Hex.ZPoly.multifactorLiftQuadratic_spec (p k : ℕ) [Hex.ZMod64.Bounds p]
  (f : Hex.ZPoly) (factors : Array Hex.ZPoly) (hk : 1 ≤ k) (hp : 1 < p)
  (hinv :
    Hex.ZPoly.QuadraticMultifactorLiftInvariant p k f factors.toList) :
  (Hex.ZPoly.multifactorLiftQuadratic p k f factors).polyProduct.congr f
    (p ^ k)
Hex.ZPoly.multifactorLiftQuadratic_spec
  (p k : ℕ) [Hex.ZMod64.Bounds p]
  (f : Hex.ZPoly)
  (factors : Array Hex.ZPoly) (hk : 1 ≤ k)
  (hp : 1 < p)
  (hinv :
    Hex.ZPoly.QuadraticMultifactorLiftInvariant
      p k f factors.toList) :
  (Hex.ZPoly.multifactorLiftQuadratic p k
          f factors).polyProduct.congr
    f (p ^ k)

The product of the lifted factors is congruent to f modulo p^k, under the recursive precondition package consumed by the quadratic multifactor lifting tree.

The lift-uniqueness companion (linear-vs-quadratic agreement after canonicalisation) lives in hex-hensel-mathlib.

The quadratic doubling loop is verified against an explicit loop invariant: the three facts a caller must maintain across one doubling (product congruence, Bezout congruence, and monicity of the leading factor) are exactly the preconditions the doubling step requires.

def

Hex.ZPoly.QuadraticLiftLoopInvariant (m : ℕ) (f : Hex.ZPoly)
  (acc : Hex.QuadraticLiftResult) : Prop
Hex.ZPoly.QuadraticLiftLoopInvariant
  (m : ℕ) (f : Hex.ZPoly)
  (acc : Hex.QuadraticLiftResult) : Prop

The proof state carried by one quadratic Hensel loop modulus m. A caller writing proofs against this invariant must supply three conjuncts, in this order:

Product congruence: acc.g * acc.h ≡ f (mod m);
Bezout congruence: acc.s * acc.g + acc.t * acc.h ≡ 1 (mod m);
Leading factor monic: acc.g is monic.

The constructor QuadraticLiftLoopInvariant.of_product_bezout_monic takes the three facts in the same order. Together they are exactly the preconditions consumed by one application of quadraticHenselStep (and, inductively, by the doubling loop in iterateQuadraticHensel).

theorem

Hex.ZPoly.quadraticLiftLoopInvariant_step (m : ℕ) (f : Hex.ZPoly)
  (acc : Hex.QuadraticLiftResult) (hm : 1 < m)
  (hinv : Hex.ZPoly.QuadraticLiftLoopInvariant m f acc) :
  have next :=
    Hex.ZPoly.quadraticHenselStep m f acc.g acc.h acc.s acc.t;
  Hex.ZPoly.QuadraticLiftLoopInvariant (m * m) f next
Hex.ZPoly.quadraticLiftLoopInvariant_step
  (m : ℕ) (f : Hex.ZPoly)
  (acc : Hex.QuadraticLiftResult)
  (hm : 1 < m)
  (hinv :
    Hex.ZPoly.QuadraticLiftLoopInvariant m
      f acc) :
  have next :=
    Hex.ZPoly.quadraticHenselStep m f
      acc.g acc.h acc.s acc.t;
  Hex.ZPoly.QuadraticLiftLoopInvariant
    (m * m) f next

One quadratic step preserves the loop invariant while replacing m by m*m.

This is the local invariant-preservation surface consumed by the quadratic doubling loop.

Monicity of the leading factor is preserved by the whole quadratic multifactor lift, so a monic input yields monic lifted factors, which the factorization pipeline requires.

theorem

Hex.ZPoly.multifactorLiftQuadratic_each_monic (p k : ℕ)
  [Hex.ZMod64.Bounds p] (f : Hex.ZPoly) (factors : Array Hex.ZPoly)
  (hk : 1 ≤ k) (hp : 1 < p) (hf_monic : Hex.DensePoly.Monic f)
  (hinv :
    Hex.ZPoly.QuadraticMultifactorLiftInvariant p k f factors.toList)
  (i : Fin (Hex.ZPoly.multifactorLiftQuadratic p k f factors).size) :
  Hex.DensePoly.Monic
    (Hex.ZPoly.multifactorLiftQuadratic p k f factors)[i]
Hex.ZPoly.multifactorLiftQuadratic_each_monic
  (p k : ℕ) [Hex.ZMod64.Bounds p]
  (f : Hex.ZPoly)
  (factors : Array Hex.ZPoly) (hk : 1 ≤ k)
  (hp : 1 < p)
  (hf_monic : Hex.DensePoly.Monic f)
  (hinv :
    Hex.ZPoly.QuadraticMultifactorLiftInvariant
      p k f factors.toList)
  (i :
    Fin
      (Hex.ZPoly.multifactorLiftQuadratic
          p k f factors).size) :
  Hex.DensePoly.Monic
    (Hex.ZPoly.multifactorLiftQuadratic p
        k f factors)[i]

Every output of multifactorLiftQuadratic is monic when the input polynomial f is monic and the quadratic multifactor lift invariant package holds.

Driven by henselLiftQuadratic_g_monic and henselLiftQuadratic_h_monic applied at each sequential split node. Consumed by the Mathlib-facing wrapper HexBerlekampZassenhausMathlib.henselLiftData_liftedFactor_monic.