theorem HexHenselMathlib.zpoly_congr_toPolynomial_map_eq (f g : Hex.ZPoly) (m : ℕ) (hcongr : f.congr g m) : have φ := Int.castRingHom (ZMod m); Polynomial.map φ (HexPolyMathlib.toPolynomial f) = Polynomial.map φ (HexPolyMathlib.toPolynomial g)

Coefficientwise executable congruence modulo m transfers to equality after mapping the corresponding Mathlib polynomials to ZMod m.

theorem HexHenselMathlib.hensel_correct (f g h : Hex.ZPoly) (p k : ℕ) [Hex.ZMod64.Bounds p] [Hex.ZMod64.PrimeModulus p] (s t : Hex.FpPoly p) (hk : 1 ≤ k) (hp : 1 < p) (hprod : (g * h).congr f p) (hbez : (s * Hex.ZPoly.modP p g + t * Hex.ZPoly.modP p h).liftToZ.congr 1 p) (hmonic : Hex.DensePoly.Monic g) (hgdeg : 0 < Hex.DensePoly.natDegree g) : have r := Hex.ZPoly.henselLift p k f g h s t; have φ := Int.castRingHom (ZMod (p ^ k)); Polynomial.map φ (HexPolyMathlib.toPolynomial r.g) * Polynomial.map φ (HexPolyMathlib.toPolynomial r.h) = Polynomial.map φ (HexPolyMathlib.toPolynomial f)

The iterative executable lift gives a factorization of f over Mathlib polynomials modulo p^k.

theorem HexHenselMathlib.hensel_extends (f g h : Hex.ZPoly) (p k : ℕ) [Hex.ZMod64.Bounds p] (s t : Hex.FpPoly p) (hk : 1 ≤ k) (_hprod : (g * h).congr f p) (_hbez : (s * Hex.ZPoly.modP p g + t * Hex.ZPoly.modP p h).liftToZ.congr 1 p) (_hmonic : Hex.DensePoly.Monic g) : have r := Hex.ZPoly.henselLift p k f g h s t; have φ := Int.castRingHom (ZMod p); Polynomial.map φ (HexPolyMathlib.toPolynomial r.g) = Polynomial.map φ (HexPolyMathlib.toPolynomial g) ∧ Polynomial.map φ (HexPolyMathlib.toPolynomial r.h) = Polynomial.map φ (HexPolyMathlib.toPolynomial h)

The iterative executable lift extends the input factorization modulo p.

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

The iterative executable lift preserves the Mathlib degree of the monic lifted factor.

theorem HexHenselMathlib.zpoly_congr_of_toPolynomial_map_eq (f g : Hex.ZPoly) (m : ℕ) (hmap : have φ := Int.castRingHom (ZMod m); Polynomial.map φ (HexPolyMathlib.toPolynomial f) = Polynomial.map φ (HexPolyMathlib.toPolynomial g)) : f.congr g m

Equality of Mathlib polynomial reductions modulo m gives the executable coefficientwise congruence used by Hex.ZPoly.

theorem HexHenselMathlib.toPolynomial_monic_of_dense_monic (f : Hex.ZPoly) (hmonic : Hex.DensePoly.Monic f) : (HexPolyMathlib.toPolynomial f).Monic

The executable monic predicate transfers to Mathlib's polynomial monic predicate.

theorem HexHenselMathlib.quadraticHenselStep_factor_correct (m : ℕ) (f g h s t : Hex.ZPoly) (hm : 0 < m) (hprod : (g * h).congr f m) (hbez : (s * g + t * h).congr 1 m) (hmonic : Hex.DensePoly.Monic g) : have r := Hex.ZPoly.quadraticHenselStep m f g h s t; have φ := Int.castRingHom (ZMod (m * m)); Polynomial.map φ (HexPolyMathlib.toPolynomial r.g) * Polynomial.map φ (HexPolyMathlib.toPolynomial r.h) = Polynomial.map φ (HexPolyMathlib.toPolynomial f)

The quadratic executable step gives a Mathlib factorization modulo m*m. This is the Mathlib-facing form of Hex.ZPoly.quadraticHenselStep_factor_spec.

theorem HexHenselMathlib.quadraticHenselStep_bezout_correct (m : ℕ) (f g h s t : Hex.ZPoly) (hm : 0 < m) (hprod : (g * h).congr f m) (hbez : (s * g + t * h).congr 1 m) (hmonic : Hex.DensePoly.Monic g) : have r := Hex.ZPoly.quadraticHenselStep m f g h s t; have φ := Int.castRingHom (ZMod (m * m)); Polynomial.map φ (HexPolyMathlib.toPolynomial r.s) * Polynomial.map φ (HexPolyMathlib.toPolynomial r.g) + Polynomial.map φ (HexPolyMathlib.toPolynomial r.t) * Polynomial.map φ (HexPolyMathlib.toPolynomial r.h) = 1

The quadratic executable step updates Bezout witnesses modulo m*m. This is the Mathlib-facing form of Hex.ZPoly.quadraticHenselStep_bezout_spec.

theorem HexHenselMathlib.quadraticHenselStep_monic (m : ℕ) (f g h s t : Hex.ZPoly) (hm : 1 < m) (hmonic : Hex.DensePoly.Monic g) : have r := Hex.ZPoly.quadraticHenselStep m f g h s t; (HexPolyMathlib.toPolynomial r.g).Monic

The quadratic step preserves monicity on the lifted g factor in Mathlib form.

The executable substrate (Hex.ZPoly.quadraticHenselStep_monic) requires 1 < m: at m = 1 every *ModSquare operation reduces modulo 1, collapsing the lifted factor to the zero polynomial, which is not monic. So the hypothesis is 1 < m.

theorem HexHenselMathlib.hensel_unique (f g h g' h' : Polynomial ℤ) (p k : ℕ) [Fact (Nat.Prime p)] (_hk : 0 < k) (hg : g.Monic) (hg' : g'.Monic) (hdeg : g.natDegree = g'.natDegree) (hprod : have φ := Int.castRingHom (ZMod (p ^ k)); Polynomial.map φ g * Polynomial.map φ h = Polynomial.map φ f) (hprod' : have φ := Int.castRingHom (ZMod (p ^ k)); Polynomial.map φ g' * Polynomial.map φ h' = Polynomial.map φ f) (hg1 : have φ := Int.castRingHom (ZMod p); Polynomial.map φ g = Polynomial.map φ g') (_hh1 : have φ := Int.castRingHom (ZMod p); Polynomial.map φ h = Polynomial.map φ h') (hcop : have φ := Int.castRingHom (ZMod p); IsCoprime (Polynomial.map φ g) (Polynomial.map φ h)) : have φ := Int.castRingHom (ZMod (p ^ k)); Polynomial.map φ g = Polynomial.map φ g' ∧ Polynomial.map φ h = Polynomial.map φ h'

Coprime monic factorizations with the same reduction modulo p are unique modulo p^k.

The 0 < k hypothesis is part of the calling convention; the proof works for k = 0 too because ZMod 1 is the zero ring. The hh1 hypothesis is similarly redundant: the cancellation step uses hg1 to substitute g' for g mod p, which suffices in conjunction with hcop and the monic degree bound.

theorem HexHenselMathlib.quadraticHenselStep_unique_mod_pow_two_mul (f g h s t : Hex.ZPoly) (g' h' : Polynomial ℤ) (p k : ℕ) [Fact (Nat.Prime p)] [Hex.ZMod64.Bounds p] (hk : 0 < k) (hprod : (g * h).congr f (p ^ k)) (hbez : (s * g + t * h).congr 1 (p ^ k)) (hmonic : Hex.DensePoly.Monic g) (hg' : g'.Monic) (hdeg : (HexPolyMathlib.toPolynomial (Hex.ZPoly.quadraticHenselStep (p ^ k) f g h s t).g).natDegree = g'.natDegree) (hprod' : have φ := Int.castRingHom (ZMod (p ^ (2 * k))); Polynomial.map φ g' * Polynomial.map φ h' = Polynomial.map φ (HexPolyMathlib.toPolynomial f)) (hg1 : have φ := Int.castRingHom (ZMod p); Polynomial.map φ (HexPolyMathlib.toPolynomial (Hex.ZPoly.quadraticHenselStep (p ^ k) f g h s t).g) = Polynomial.map φ g') (hh1 : have φ := Int.castRingHom (ZMod p); Polynomial.map φ (HexPolyMathlib.toPolynomial (Hex.ZPoly.quadraticHenselStep (p ^ k) f g h s t).h) = Polynomial.map φ h') (hcop : have φ := Int.castRingHom (ZMod p); IsCoprime (Polynomial.map φ (HexPolyMathlib.toPolynomial (Hex.ZPoly.quadraticHenselStep (p ^ k) f g h s t).g)) (Polynomial.map φ (HexPolyMathlib.toPolynomial (Hex.ZPoly.quadraticHenselStep (p ^ k) f g h s t).h))) : have r := Hex.ZPoly.quadraticHenselStep (p ^ k) f g h s t; have φ := Int.castRingHom (ZMod (p ^ (2 * k))); Polynomial.map φ (HexPolyMathlib.toPolynomial r.g) = Polynomial.map φ g' ∧ Polynomial.map φ (HexPolyMathlib.toPolynomial r.h) = Polynomial.map φ h'

Quadratic lifting is compatible with the Mathlib uniqueness theorem at the doubled prime-power precision.

@[irreducible]

def HexHenselMathlib.ZCoprimeSplits (p : ℕ) [Hex.ZMod64.Bounds p] : List Hex.ZPoly → Prop

Guarded-tree split coprimality over ZPoly, stated directly on the integer polynomials (via their modP images) rather than on the FpPoly factors. This is the ZPoly-level analogue of QuadraticMultifactorCoprimeSplits used to transport arbitrary monic factor lists (as arise in the linear/quadratic agreement) into the balanced quadratic invariant.

Equations

• One or more equations did not get rendered due to their size.
• HexHenselMathlib.ZCoprimeSplits p [] = True
• HexHenselMathlib.ZCoprimeSplits p [_g] = True

theorem HexHenselMathlib.inv_of_ZCoprimeSplits (p k : ℕ) [Hex.ZMod64.Bounds p] [Hex.ZMod64.PrimeModulus p] (f : Hex.ZPoly) (factors : List Hex.ZPoly) (hp : 1 < p) (hk : 1 ≤ k) (hfactors_monic : ∀ g ∈ factors, Hex.DensePoly.Monic g) (hproduct : factors.toArray.polyProduct.congr f p) (hcop : ZCoprimeSplits p factors) (hne : factors ≠ []) : Hex.ZPoly.QuadraticMultifactorLiftInvariant p k f factors

Build the guarded quadratic multifactor lift invariant from ZPoly-level boundary facts: monic factors, split coprimality (ZCoprimeSplits), and the lifted product congruence modulo p. No monic-target hypothesis is required; the balanced invariant constrains only the leading factor of each split, which is a product of the (monic) input factors.

theorem HexHenselMathlib.quadraticMultifactorLiftInvariant_of_multifactorLiftInvariant (p k : ℕ) [Fact (Nat.Prime p)] [Hex.ZMod64.Bounds p] [Hex.ZMod64.PrimeModulus p] (f : Hex.ZPoly) (factors : List Hex.ZPoly) (hk : 1 ≤ k) (hmonic : ∀ g ∈ factors, Hex.DensePoly.Monic g) (hinv : Hex.ZPoly.MultifactorLiftInvariant p k f factors) : Hex.ZPoly.QuadraticMultifactorLiftInvariant p k f factors

The linear multifactor invariant can initialise the quadratic multifactor invariant when every raw input head is monic.

theorem HexHenselMathlib.multifactorLift_eq_multifactorLiftQuadratic (p k : ℕ) [Fact (Nat.Prime p)] [Hex.ZMod64.Bounds p] [Hex.ZMod64.PrimeModulus p] (f : Hex.ZPoly) (factors : Array Hex.ZPoly) (hk : 1 ≤ k) (hp : 1 < p) (hmonic : ∀ g ∈ factors.toList, Hex.DensePoly.Monic g) (hinv : Hex.ZPoly.MultifactorLiftInvariant p k f factors.toList) : have φ := Int.castRingHom (ZMod (p ^ k)); List.map (fun (g : Hex.DensePoly ℤ) => Polynomial.map φ (HexPolyMathlib.toPolynomial g)) (Hex.ZPoly.multifactorLift p k f factors).toList = List.map (fun (g : Hex.DensePoly ℤ) => Polynomial.map φ (HexPolyMathlib.toPolynomial g)) (Hex.ZPoly.multifactorLiftQuadratic p k f factors).toList

The linear and quadratic multifactor lifters agree modulo p ^ k after canonical reduction, when both are applied to the same input under the recursive MultifactorLiftInvariant precondition consumed by both Hex.ZPoly.multifactorLift_spec and Hex.ZPoly.multifactorLiftQuadratic_spec.

The result is stated over the public array/product multifactor surface rather than the private split-tree helpers, and is expressed in Mathlib form via Polynomial.map (Int.castRingHom (ZMod (p ^ k))). Through zpoly_congr_toPolynomial_map_eq / zpoly_congr_of_toPolynomial_map_eq, this is equivalent to per-factor canonicalisation by Hex.ZPoly.reduceModPow _ p k.

The raw-head monicity hypothesis hmonic is required: it pins each split head's Mathlib degree so hensel_unique can identify the linear and quadratic lifts. See multifactorLiftList_map_eq_quadratic for the congruent-target induction behind the proof.

This proves the lift-uniqueness correspondence between the executable hex-hensel algorithms and their Mathlib polynomial interpretations.