def Array.polyProduct (factors : Array Hex.ZPoly) : Hex.ZPoly

Ordered product of integer polynomial factors, using left-fold order.

Equations

• factors.polyProduct = Array.foldl (fun (x1 x2 : Hex.ZPoly) => x1 * x2) 1 factors

def Hex.ZPoly.normalizedXGCD (p : Nat) [ZMod64.Bounds p] (g h : ZPoly) : DensePoly.XGCDResult (ZMod64 p)

Extended gcd witnesses scaled so their Bezout combination is monic when the raw Euclidean gcd is a nonzero constant unit.

Equations

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

theorem Hex.ZPoly.normalizedXGCD_bezout (p : Nat) [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (g h : ZPoly) : have xgcd := normalizedXGCD p g h; xgcd.left * modP p g + xgcd.right * modP p h = xgcd.gcd

The normalised xgcd witnesses still satisfy the Bezout identity, now for the normalised gcd component.

theorem Hex.ZPoly.normalizedXGCD_liftToZ_bezout_congr_of_gcd_eq_one (p : Nat) [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (g h : ZPoly) (hgcd : have xgcd := normalizedXGCD p g h; xgcd.gcd = 1) : have xgcd := normalizedXGCD p g h; (FpPoly.liftToZ xgcd.left * g + FpPoly.liftToZ xgcd.right * h).congr 1 p

If the normalised xgcd component is 1, its lifted witnesses give the integer-polynomial Bezout congruence needed to initialise a Hensel split.

def Hex.ZPoly.multifactorLiftList (p k : Nat) [ZMod64.Bounds p] (f : ZPoly) : List ZPoly → Array ZPoly

Recursive list-shape worker behind multifactorLift. At each non-singleton step it lifts the head factor g against the running complementary product Array.polyProduct rest.toArray via henselLift, and recurses with lifted.h as the new target on rest. The singleton case returns the input reduced modulo p^k; the empty case returns the empty array.

Equations

• One or more equations did not get rendered due to their size.
• Hex.ZPoly.multifactorLiftList p k f [] = #[]
• Hex.ZPoly.multifactorLiftList p k f [_g] = #[f.reduceModPow p k]

def Hex.ZPoly.multifactorLift (p k : Nat) [ZMod64.Bounds p] (f : ZPoly) (factors : Array ZPoly) : Array ZPoly

Lift an ordered array of factors from congruence modulo p to congruence modulo p^k.

Equations

• Hex.ZPoly.multifactorLift p k f factors = Hex.ZPoly.multifactorLiftList p k f factors.toList

def Hex.ZPoly.MultifactorLiftInvariant (p k : Nat) [ZMod64.Bounds p] (f : ZPoly) : List ZPoly → Prop

Recursive preconditions required by the sequential multifactor lift.

In the g :: h :: tail arm, the four conjuncts are exactly the inputs henselLift_spec consumes for the binary split of g against the running complementary product Array.polyProduct (h :: tail).toArray, followed by the recursive precondition for the lifted complement:

1. LinearLiftLoopInvariant at n = 1; initial state for the linear loop;

2. the step-degree invariant at every iteration n ≥ 1;

3. the step-Bezout congruence at every iteration n ≥ 1;

4. MultifactorLiftInvariant for the recursive tail with lifted.h as the new target.

The base cases impose the trivial obligations: congr 1 f (p ^ k) for the empty list and no preconditions for a singleton.

This invariant is proof-internal: it is the correctness substrate consumed by multifactorLift_spec and by the Mathlib-side lift-uniqueness statement HexHenselMathlib.multifactorLift_eq_multifactorLiftQuadratic, and is not intended to be constructed directly by external callers. Unlike the quadratic path, no multifactorLiftInvariant_of_factorsModP smart constructor is provided: the four-conjunct shape mentions per-iteration LinearLiftLoopInvariant and LinearLiftStepDegreeInvariant quantifications that would require substrate lemmas (an of_product_bezout_monic constructor for LinearLiftLoopInvariant, plus henselLift_h_congr_mod_base and henselLift_h_monic analogues of the quadratic recursive correspondence) that HexHensel/Linear.lean does not currently expose.

Callers wanting a consumer-facing Hensel-lift correctness surface should use the quadratic flavour QuadraticMultifactorLiftInvariant, constructed from natural mod-p factorisation facts by quadraticMultifactorLiftInvariant_of_factorsModP (with the QuadraticMultifactorLiftInvariant_of_choosePrimeData wrapper at the Berlekamp-Zassenhaus boundary). The executable Berlekamp-Zassenhaus computation already uses the quadratic invariant exclusively (HexBerlekampZassenhaus/Basic.lean). A Mathlib-side downstream caller that needs the linear-path lifted factors modulo p^k should obtain them via HexHenselMathlib.multifactorLift_eq_multifactorLiftQuadratic, which equates the two paths under the Mathlib Polynomial.map (Int.castRingHom (ZMod (p^k))) canonicalisation.

Equations

• One or more equations did not get rendered due to their size.
• Hex.ZPoly.MultifactorLiftInvariant p k f [] = Hex.ZPoly.congr 1 f (p ^ k)
• Hex.ZPoly.MultifactorLiftInvariant p k f [_g] = True

@[simp]

theorem Hex.ZPoly.one_mul_zpoly (g : ZPoly) : 1 * g = g

Left identity for ZPoly multiplication, used to reason about Array.polyProduct as a left fold from 1. Shared by the linear and quadratic multifactor proofs.

@[simp]

theorem Hex.ZPoly.polyProduct_singleton (g : ZPoly) : #[g].polyProduct = g

Array.polyProduct of a singleton array is just the element.

theorem Hex.ZPoly.list_foldl_mul_eq_mul_foldl_one (g : ZPoly) (xs : List ZPoly) : List.foldl (fun (acc factor : ZPoly) => acc * factor) g xs = g * List.foldl (fun (acc factor : ZPoly) => acc * factor) 1 xs

Associativity helper for product invariants: folding (· * ·) over a List ZPoly with seed g factors out as g times the same fold with seed 1. This is not a simp normal form because both sides contain the same left fold.

theorem Hex.ZPoly.polyProduct_singleton_append (g : ZPoly) (rest : Array ZPoly) : (#[g] ++ rest).polyProduct = g * rest.polyProduct

Splitting Array.polyProduct across a singleton prepend: the head factors out as a left multiplication. Used to relate the multifactor recursion tree to the public ordered-product convention. Left untagged as @[simp] because downstream Mathlib-side proofs use large recursive product terms where this rewrite is better applied explicitly.

@[simp]

theorem Hex.ZPoly.polyProduct_empty : #[].polyProduct = 1

Array.polyProduct of the empty array is the multiplicative unit.

@[simp]

theorem Hex.ZPoly.polyProduct_append (xs ys : Array ZPoly) : (xs ++ ys).polyProduct = xs.polyProduct * ys.polyProduct

Array.polyProduct splits as a product across array concatenation.

theorem Hex.ZPoly.polyProduct_cons_toArray (g : ZPoly) (rest : List ZPoly) : (g :: rest).toArray.polyProduct = g * rest.toArray.polyProduct

Array.polyProduct over (g :: rest).toArray factors the head out as a left multiplication. The List-flavoured analogue of polyProduct_singleton_append. Left untagged as @[simp] for the same downstream performance reason: callers use it explicitly at product-splitting points.

@[simp]

theorem Hex.ZPoly.polyProduct_pair (g h : ZPoly) : #[g, h].polyProduct = g * h

Array.polyProduct of a two-element array is the product of the two entries.

@[simp]

theorem Hex.ZPoly.polyProduct_replicate_zero_toArray (g : ZPoly) : (List.replicate 0 g).toArray.polyProduct = 1

Array.polyProduct over a zero-length replicated list is the multiplicative unit.

theorem Hex.ZPoly.multifactorLift_spec (p k : Nat) [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : ZPoly) (factors : Array ZPoly) (hk : 1 ≤ k) (hp : 1 < p) (hinv : MultifactorLiftInvariant p k f factors.toList) : (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.