8.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 forward theorem QuadraticLiftLoopInvariant.of_product_bezout_monic takes the three facts in the same order. Together they are exactly the preconditions consumed by one application of Hex.ZPoly.quadraticHenselStep and, inductively, by the exact-exponent recursion.

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 lift recursion.

Monicity of the leading factor is preserved by the whole quadratic multifactor lift, so a monic input yields monic lifted factors, which the factorization algorithm 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 Hex.ZPoly.multifactorLiftQuadratic is monic when the input polynomial f is monic and the quadratic multifactor lift invariant package holds.

The proof applies Hex.ZPoly.henselLiftFactors_fst_monic and Hex.ZPoly.henselLiftFactors_snd_monic at each balanced split node, providing the monicness fact used by the Mathlib-facing wrapper.