def Hex.ZPoly.quadraticDoublingSteps (k : Nat) : Nat

Number of quadratic-doubling steps needed to reach precision p^k from data valid modulo p. Returns 0 when k ≤ 1 (no doubling needed) and ⌊log₂ (k - 1)⌋ + 1 otherwise, the least n with k ≤ 2 ^ n. This remains the public fuel bound used by downstream recombination searches.

Equations

• Hex.ZPoly.quadraticDoublingSteps k = if k ≤ 1 then 0 else (k - 1).log2 + 1

@[simp]

theorem Hex.ZPoly.quadraticDoublingSteps_zero : quadraticDoublingSteps 0 = 0

Zero requested precision needs no quadratic doubling steps.

@[simp]

theorem Hex.ZPoly.quadraticDoublingSteps_one : quadraticDoublingSteps 1 = 0

Precision p^1 is the input precision, so it needs no doubling steps.

def Hex.ZPoly.reduceLift (p k : Nat) [ZMod64.Bounds p] (r : QuadraticLiftResult) : QuadraticLiftResult

Canonicalise every component of a quadratic lift at precision p^k.

Equations

• Hex.ZPoly.reduceLift p k r = { g := r.g.reduceModPow p k, h := r.h.reduceModPow p k, s := r.s.reduceModPow p k, t := r.t.reduceModPow p k }

@[irreducible]

def Hex.ZPoly.liftExact (p : Nat) [ZMod64.Bounds p] (f : ZPoly) (k : Nat) : QuadraticLiftResult → QuadraticLiftResult

Return a lift reduced at exactly exponent k. Recursing through ceil(k / 2) limits a correction's transient working exponent to k when even and k + 1 when odd, instead of the next power of two.

This is the specification; liftExactImpl is the compiled shape.

Equations

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

@[irreducible]

def Hex.ZPoly.liftExactImpl (p : Nat) [ZMod64.Bounds p] (f : ZPoly) (k : Nat) : QuadraticLiftResult → QuadraticLiftResult

Runtime shape of liftExact, dropping the canonicalisation that reduceLift_step_eq_of_even proves redundant. For even k the preceding step runs at modulus p^(k/2) and returns coefficients already canonical modulo (p^(k/2))^2 = p^k; only an odd k, whose step overshoots to p^(k+1), needs the descent back to p^k. Proved equal to liftExact in liftExact_eq_impl.

Equations

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

@[csimp]

theorem Hex.ZPoly.liftExact_eq_impl : liftExact = liftExactImpl

Proof-backed compiled implementation of the exact-exponent quadratic recursion.

def Hex.ZPoly.henselLiftQuadratic (p k : Nat) [ZMod64.Bounds p] (f g h s t : ZPoly) : QuadraticLiftResult

Lift a Bezout-witnessed factorisation modulo p to one valid modulo p^k by iterating quadraticHenselStep at exact requested exponents.

Each recursive level first reaches p^ceil(k/2), doubles once, and reduces to p^k. This uses the same logarithmic number of quadratic steps as the power-of-two schedule while avoiding excess big-integer precision.

Equations

• Hex.ZPoly.henselLiftQuadratic p k f g h s t = Hex.ZPoly.liftExact p f k { g := g, h := h, s := s, t := t }

def Hex.ZPoly.henselLiftFactors (p k : Nat) [ZMod64.Bounds p] (f g h s t : ZPoly) : ZPoly × ZPoly

Exact-exponent lift of only the final two factors. Earlier levels retain Bezout witnesses for the next correction; the last level omits the witness update because multifactor recursion consumes only the two factors.

Equations

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

def Hex.ZPoly.henselLiftFactorsImpl (p k : Nat) [ZMod64.Bounds p] (f g h s t : ZPoly) : ZPoly × ZPoly

Runtime shape of henselLiftFactors. The final factor-only step obeys the same coefficient-range invariant as the full step (quadraticHenselFactors_canonical), so for even k the closing pair of reductions is the identity. Proved equal to henselLiftFactors in henselLiftFactors_eq_impl.

Equations

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

@[csimp]

theorem Hex.ZPoly.henselLiftFactors_eq_impl : henselLiftFactors = henselLiftFactorsImpl

Proof-backed compiled implementation of the factor-only exact lift.

theorem Hex.ZPoly.henselLiftFactors_eq (p k : Nat) [ZMod64.Bounds p] (f g h s t : ZPoly) : henselLiftFactors p k f g h s t = ((henselLiftQuadratic p k f g h s t).g, (henselLiftQuadratic p k f g h s t).h)

The factor-only final step is byte-identical to projecting the full lift.

theorem Hex.ZPoly.henselLiftFactors_fst (p k : Nat) [ZMod64.Bounds p] (f g h s t : ZPoly) : (henselLiftFactors p k f g h s t).fst = (henselLiftQuadratic p k f g h s t).g

theorem Hex.ZPoly.henselLiftFactors_snd (p k : Nat) [ZMod64.Bounds p] (f g h s t : ZPoly) : (henselLiftFactors p k f g h s t).snd = (henselLiftQuadratic p k f g h s t).h

theorem Hex.ZPoly.henselLiftFactors_canonical (p k : Nat) [ZMod64.Bounds p] (f g h s t : ZPoly) : (henselLiftFactors p k f g h s t).fst.Canonical (p ^ k) ∧ (henselLiftFactors p k f g h s t).snd.Canonical (p ^ k)

Both outputs of the factor-only exact lift are canonical modulo p^k: either branch of henselLiftFactors ends in ZPoly.reduceModPow _ p k.

This is what lets the multifactor tree skip the reduction at every leaf below the root, since each recursive call's target is a henselLiftFactors output.

def Hex.ZPoly.factorDegreeSum (factors : List ZPoly) : Nat

Sum of polynomial degrees used to estimate the work on one side of a multifactor Hensel split.

Equations

• Hex.ZPoly.factorDegreeSum factors = List.foldl (fun (total : Nat) (g : Hex.ZPoly) => total + Hex.DensePoly.natDegree g) 0 factors

def Hex.ZPoly.factorMaxDegree (factors : List ZPoly) : Nat

Largest polynomial degree in a prospective multifactor Hensel node.

Equations

• Hex.ZPoly.factorMaxDegree factors = List.foldl (fun (largest : Nat) (g : Hex.ZPoly) => max largest (Hex.DensePoly.natDegree g)) 0 factors

def Hex.ZPoly.factorDegreeStats (factors : List ZPoly) : Nat × Nat

Total and largest degree in one traversal.

Equations

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

def Hex.ZPoly.splitImbalance (factors : List ZPoly) (i : Nat) : Nat

Degree imbalance produced by splitting factors at i.

Equations

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

def Hex.ZPoly.balancedSplitIndex (factors : List ZPoly) : Nat

Choose a nontrivial prefix split of the factor order supplied to a multifactor Hensel node. When one modular factor has more than half the total degree, choose the prefix split whose two total degrees are closest; this avoids recursively pairing that dominant factor with a much smaller neighbour when the incoming order permits it. Otherwise keep the count-halving tree, whose deliberately unbalanced degree splits can make the root XGCD much cheaper. The final clamp makes the result valid for every list of length at least two, independently of the degree data.

This definition is deliberately opaque across module boundaries: downstream proofs should use balancedSplitIndex_pos and balancedSplitIndex_lt_length, rather than unfold the runtime heuristic.

Equations

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

theorem Hex.ZPoly.balancedSplitIndex_pos (factors : List ZPoly) : 0 < balancedSplitIndex factors

The balanced split leaves at least one factor on its left.

theorem Hex.ZPoly.balancedSplitIndex_lt_length (factors : List ZPoly) (h : 2 ≤ factors.length) : balancedSplitIndex factors < factors.length

A balanced split of at least two factors leaves at least one factor on its right.

@[irreducible]

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

Recursive list-shape worker behind multifactorLiftQuadratic, shaped as a count-balanced product tree except where a dominant-degree factor calls for a degree-aware split. At each non-singleton step it lifts the left product g against the right product h via henselLiftFactors, then recurses into both sides with the lifted sub-products as the new targets. The two recursive outputs are concatenated L-then-R, so the returned array stays in the original factor order. The singleton case returns the input reduced modulo p^k; the empty case returns the empty array. Every output is the same reduced value because the Hensel lift is unique modulo p^k.

Equations

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

@[irreducible]

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

Runtime shape of multifactorLiftQuadraticList. The extra canonical flag records whether the incoming target is already reduced modulo p^k. Every recursive call passes a henselLiftFactors output, which henselLiftFactors_canonical shows is canonical, so only the root -- the one target the caller supplies as an arbitrary integer polynomial -- can still need the leaf reduction. Every singleton subtree below a split therefore drops one full-precision reduction; on a two-factor lift at odd precision that is both output factors. Proved equal to multifactorLiftQuadraticList in multifactorLiftQuadraticList_eq_impl.

Equations

• One or more equations did not get rendered due to their size.
• Hex.ZPoly.multifactorLiftQuadraticListImpl p k canonical f [] = #[]
• Hex.ZPoly.multifactorLiftQuadraticListImpl p k canonical f [_g] = #[if canonical = true then f else f.reduceModPow p k]

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

Root entry point of the compiled tree walk: the caller's target is an arbitrary integer polynomial, so the root leaf still reduces.

Equations

• Hex.ZPoly.multifactorLiftQuadraticListRoot p k f factors = Hex.ZPoly.multifactorLiftQuadraticListImpl p k false f factors

@[csimp]

theorem Hex.ZPoly.multifactorLiftQuadraticList_eq_impl : multifactorLiftQuadraticList = multifactorLiftQuadraticListRoot

Proof-backed compiled implementation of the multifactor tree walk.

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

Quadratic multifactor Hensel lift.

Lifts an ordered array of factors of f from congruence modulo p to congruence modulo p^k using the doubling step Hex.ZPoly.quadraticHenselStep inside the guarded multifactor product tree.

Equations

• Hex.ZPoly.multifactorLiftQuadratic p k f factors = Hex.ZPoly.multifactorLiftQuadraticList p k f factors.toList

def Hex.ZPoly.QuadraticLiftLoopInvariant (m : Nat) (f : ZPoly) (acc : 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:

1. Product congruence: acc.g * acc.h ≡ f (mod m);

2. Bezout congruence: acc.s * acc.g + acc.t * acc.h ≡ 1 (mod m);

3. 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.

Equations

• Hex.ZPoly.QuadraticLiftLoopInvariant m f acc = ((acc.g * acc.h).congr f m ∧ (acc.s * acc.g + acc.t * acc.h).congr 1 m ∧ Hex.DensePoly.Monic acc.g)

theorem Hex.ZPoly.QuadraticLiftLoopInvariant.of_product_bezout_monic {m : Nat} {f g h s t : ZPoly} (hprod : (g * h).congr f m) (hbezout : (s * g + t * h).congr 1 m) (hg_monic : DensePoly.Monic g) : QuadraticLiftLoopInvariant m f { g := g, h := h, s := s, t := t }

Constructor for the initial quadratic split invariant from the three proof obligations supplied by factor-product, Bezout, and monicness facts.

@[simp]

theorem Hex.ZPoly.QuadraticLiftLoopInvariant.prod_congr {m : Nat} {f : ZPoly} {acc : QuadraticLiftResult} (h : QuadraticLiftLoopInvariant m f acc) : (acc.g * acc.h).congr f m

Product-congruence projection of QuadraticLiftLoopInvariant.

@[simp]

theorem Hex.ZPoly.QuadraticLiftLoopInvariant.bezout_congr {m : Nat} {f : ZPoly} {acc : QuadraticLiftResult} (h : QuadraticLiftLoopInvariant m f acc) : (acc.s * acc.g + acc.t * acc.h).congr 1 m

Bezout-congruence projection of QuadraticLiftLoopInvariant.

@[simp]

theorem Hex.ZPoly.QuadraticLiftLoopInvariant.monic {m : Nat} {f : ZPoly} {acc : QuadraticLiftResult} (h : QuadraticLiftLoopInvariant m f acc) : DensePoly.Monic acc.g

Monicness projection of QuadraticLiftLoopInvariant: the leading factor acc.g is monic.

theorem Hex.ZPoly.quadraticLiftLoopInvariant_step (m : Nat) (f : ZPoly) (acc : QuadraticLiftResult) (hm : 1 < m) (hinv : QuadraticLiftLoopInvariant m f acc) : have next := quadraticHenselStep m f acc.g acc.h acc.s acc.t; 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.

theorem Hex.ZPoly.le_two_pow_quadraticDoublingSteps (k : Nat) : k ≤ 2 ^ quadraticDoublingSteps k

The doubling count reaches the requested precision exponent.

After quadraticDoublingSteps k iterations from precision exponent 1, the quadratic wrapper has reached exponent 2 ^ quadraticDoublingSteps k, which is at least k.

theorem Hex.ZPoly.henselLiftQuadratic_h_congr_mod_base (p k : Nat) [ZMod64.Bounds p] (f g h s t : ZPoly) (hk : 1 ≤ k) (hp : 1 < p) (hinv : QuadraticLiftLoopInvariant p f { g := g, h := h, s := s, t := t }) : (henselLiftQuadratic p k f g h s t).h.congr h p

The cofactor produced by henselLiftQuadratic is congruent to the input cofactor modulo p. Every exact-exponent step adjusts h by a multiple of the current modulus, and canonical reduction preserves the base congruence.

This is the surface used downstream by the multifactor _of_factorsModP boundary theorem: it lets the recursive call on lifted.h, rest reuse the same mod-p product hypothesis the caller supplies for the head split.

theorem Hex.ZPoly.henselLiftQuadratic_g_congr_mod_base (p k : Nat) [ZMod64.Bounds p] (f g h s t : ZPoly) (hk : 1 ≤ k) (hp : 1 < p) (hinv : QuadraticLiftLoopInvariant p f { g := g, h := h, s := s, t := t }) : (henselLiftQuadratic p k f g h s t).g.congr g p

The leading factor produced by henselLiftQuadratic is congruent to the input leading factor modulo p. Parallel to henselLiftQuadratic_h_congr_mod_base; used downstream to show each output of multifactorLiftQuadratic reduces mod p to its corresponding input factor.

theorem Hex.ZPoly.henselLiftFactors_fst_congr_mod_base (p k : Nat) [ZMod64.Bounds p] (f g h s t : ZPoly) (hk : 1 ≤ k) (hp : 1 < p) (hinv : QuadraticLiftLoopInvariant p f { g := g, h := h, s := s, t := t }) : (henselLiftFactors p k f g h s t).fst.congr g p

The factor-only lift's left result retains the input factor modulo p.

theorem Hex.ZPoly.henselLiftFactors_snd_congr_mod_base (p k : Nat) [ZMod64.Bounds p] (f g h s t : ZPoly) (hk : 1 ≤ k) (hp : 1 < p) (hinv : QuadraticLiftLoopInvariant p f { g := g, h := h, s := s, t := t }) : (henselLiftFactors p k f g h s t).snd.congr h p

The factor-only lift's right result retains the input cofactor modulo p.

theorem Hex.ZPoly.henselLiftQuadratic_spec (p k : Nat) [ZMod64.Bounds p] (f g h s t : ZPoly) (hk : 1 ≤ k) (hp : 1 < p) (hinv : QuadraticLiftLoopInvariant p f { g := g, h := h, s := s, t := t }) : have lifted := henselLiftQuadratic p k f g h s t; (lifted.g * lifted.h).congr f (p ^ k)

Public correctness contract for the binary quadratic wrapper: starting from a QuadraticLiftLoopInvariant p f { g, h, s, t }, the lifted pair satisfies lifted.g * lifted.h ≡ f (mod p^k).

theorem Hex.ZPoly.henselLiftFactors_spec (p k : Nat) [ZMod64.Bounds p] (f g h s t : ZPoly) (hk : 1 ≤ k) (hp : 1 < p) (hinv : QuadraticLiftLoopInvariant p f { g := g, h := h, s := s, t := t }) : ((henselLiftFactors p k f g h s t).fst * (henselLiftFactors p k f g h s t).snd).congr f (p ^ k)

The factor-only exact lift multiplies to the target modulo p^k.

theorem Hex.ZPoly.henselLiftQuadratic_bezout_spec (p k : Nat) [ZMod64.Bounds p] (f g h s t : ZPoly) (hk : 1 ≤ k) (hp : 1 < p) (hinv : QuadraticLiftLoopInvariant p f { g := g, h := h, s := s, t := t }) : have lifted := henselLiftQuadratic p k f g h s t; (lifted.s * lifted.g + lifted.t * lifted.h).congr 1 (p ^ k)

Public Bezout-pair contract for the binary quadratic wrapper. The lifted Bezout pair remains valid modulo the exact requested precision p^k.

@[irreducible]

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

Recursive preconditions required by the guarded quadratic multifactor tree.

In the non-singleton arm the factor list is split at balancedSplitIndex; the three conjuncts are exactly the inputs henselLiftFactors_spec consumes for the binary split of the left product g := Array.polyProduct L.toArray against the right product h := Array.polyProduct R.toArray, followed by the recursive preconditions for each lifted sub-product:

1. QuadraticLiftLoopInvariant at modulus p; initial state package (product congruence, Bezout, monicness) for the binary exact lift;

2. QuadraticMultifactorLiftInvariant for the left half with lifted.1 as the new target;

3. QuadraticMultifactorLiftInvariant for the right half with lifted.2 as the new target.

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

Equations

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

@[irreducible]

def Hex.ZPoly.QuadraticMultifactorCoprimeSplits (p : Nat) [ZMod64.Bounds p] : List (FpPoly p) → Prop

The split-coprimality boundary data needed to initialise every quadratic split in the balanced multifactor tree from factors modulo p.

In the non-singleton arm the factor list is split at balancedSplitIndex, and the requirement is that the normalised XGCD of the left lifted product Array.polyProduct ((L.map FpPoly.liftToZ).toArray) against the right lifted product Array.polyProduct ((R.map FpPoly.liftToZ).toArray) returns gcd = 1 in FpPoly p, and that the same coprimality holds recursively on each half. The base cases (empty list, singleton) are vacuous.

Consumed by quadraticMultifactorLiftInvariant_of_factorsModP: the per-split gcd = 1 lifts via normalizedXGCD_liftToZ_bezout_congr_of_gcd_eq_one into the Bezout half of QuadraticLiftLoopInvariant.

Equations

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

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

theorem Hex.ZPoly.monic_of_congr_mul_monic_monic {g h f : ZPoly} {m : Nat} (hm : 1 < m) (hcongr : (g * h).congr f m) (hg_monic : DensePoly.Monic g) (hf_monic : DensePoly.Monic f) (hh_bound_lt : ∀ (i : Nat), DensePoly.coeff h i < Int.ofNat m) (hh_bound_nonneg : ∀ (i : Nat), 0 ≤ DensePoly.coeff h i) (hh_ne_zero : h ≠ 0) : DensePoly.Monic h

If a bounded nonnegative cofactor h satisfies a coefficientwise congruence g * h ≡ f (mod m) against monic g and f, then h is monic. The proof compares the possible top coefficient of g * h with the top coefficient of f; the coefficient bounds rule out wraparound modulo m.

Consumed by monic_reduceModPow_of_congr_mul_monic_monic, which specialises this to the reduceModPow-canonicalised cofactor consumed by henselLiftQuadratic_h_monic.

theorem Hex.ZPoly.monic_reduceModPow_of_congr_mul_monic_monic {g h f : ZPoly} {p k : Nat} (hm : 1 < p ^ k) (hcongr : (g * h.reduceModPow p k).congr f (p ^ k)) (hg_monic : DensePoly.Monic g) (hf_monic : DensePoly.Monic f) (hh_ne_zero : h.reduceModPow p k ≠ 0) : DensePoly.Monic (h.reduceModPow p k)

Specialisation of monic_of_congr_mul_monic_monic for cofactors already canonicalised by Hex.ZPoly.reduceModPow; its coefficients automatically lie in [0, p^k).

Consumed by henselLiftQuadratic_h_monic, where the correctness congruence (lifted.g * lifted.h) ≡ f (mod p^k) already supplies a reduceModPow-form cofactor.

theorem Hex.ZPoly.henselLiftQuadratic_g_monic (p k : Nat) [ZMod64.Bounds p] (f g h s t : ZPoly) (hk : 1 ≤ k) (hp : 1 < p) (hinv : QuadraticLiftLoopInvariant p f { g := g, h := h, s := s, t := t }) : DensePoly.Monic (henselLiftQuadratic p k f g h s t).g

The lifted monic factor lifted.g produced by henselLiftQuadratic is monic. The exact-exponent recursion preserves Monic acc.g via quadraticHenselStep_monic; each reduceModPow cleanup preserves it via reduceModPow_monic_of_monic.

Consumed (alongside henselLiftQuadratic_h_monic) by multifactorLiftQuadratic_each_monic to discharge per-output monicness inside the balanced split tree.

theorem Hex.ZPoly.henselLiftQuadratic_h_monic (p k : Nat) [ZMod64.Bounds p] (f g h s t : ZPoly) (hk : 1 ≤ k) (hp : 1 < p) (hf_monic : DensePoly.Monic f) (hinv : QuadraticLiftLoopInvariant p f { g := g, h := h, s := s, t := t }) : DensePoly.Monic (henselLiftQuadratic p k f g h s t).h

The lifted cofactor lifted.h produced by henselLiftQuadratic is monic when f is monic. Derived from the cofactor monic lemma monic_reduceModPow_of_congr_mul_monic_monic applied to the correctness congruence (lifted.g * lifted.h) ≡ f (mod p^k) and henselLiftQuadratic_g_monic.

Consumed (alongside henselLiftQuadratic_g_monic) by multifactorLiftQuadratic_each_monic to discharge per-output monicness inside the balanced split tree.

theorem Hex.ZPoly.henselLiftFactors_fst_monic (p k : Nat) [ZMod64.Bounds p] (f g h s t : ZPoly) (hk : 1 ≤ k) (hp : 1 < p) (hinv : QuadraticLiftLoopInvariant p f { g := g, h := h, s := s, t := t }) : DensePoly.Monic (henselLiftFactors p k f g h s t).fst

The left factor of the factor-only lift is monic.

theorem Hex.ZPoly.henselLiftFactors_snd_monic (p k : Nat) [ZMod64.Bounds p] (f g h s t : ZPoly) (hk : 1 ≤ k) (hp : 1 < p) (hf_monic : DensePoly.Monic f) (hinv : QuadraticLiftLoopInvariant p f { g := g, h := h, s := s, t := t }) : DensePoly.Monic (henselLiftFactors p k f g h s t).snd

The right factor of the factor-only lift is monic when the target is.

theorem Hex.ZPoly.monic_one : DensePoly.Monic 1

The constant polynomial 1 is monic.

theorem Hex.ZPoly.monic_mul {a b : ZPoly} (ha : DensePoly.Monic a) (hb : DensePoly.Monic b) : DensePoly.Monic (a * b)

A product of monic integer polynomials is monic.

theorem Hex.ZPoly.monic_polyProduct_toArray (l : List ZPoly) (h : ∀ (g : ZPoly), g ∈ l → DensePoly.Monic g) : DensePoly.Monic l.toArray.polyProduct

The Array.polyProduct of a list of monic integer polynomials is monic. Needed because a balanced split multiplies a whole half of the factor list into each side of the binary Hensel step, so the leading factor is a product rather than a single input factor.

theorem Hex.ZPoly.polyProduct_map_liftToZ_append (p : Nat) [ZMod64.Bounds p] (L R : List (FpPoly p)) : (List.map FpPoly.liftToZ L).toArray.polyProduct * (List.map FpPoly.liftToZ R).toArray.polyProduct = (List.map FpPoly.liftToZ (L ++ R)).toArray.polyProduct

The lifted product splits across a list concatenation: multiplying the lifted products of two halves equals the lifted product of the concatenation. This is the algebraic content that lets a balanced split's two sub-products recombine to the whole modular product.

theorem Hex.ZPoly.quadraticMultifactorLiftInvariant_of_factorsModP (p k : Nat) [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : ZPoly) (factors : List (FpPoly p)) (hp : 1 < p) (hk : 1 ≤ k) (hf_monic : DensePoly.Monic f) (hfactors_monic : ∀ (g : FpPoly p), g ∈ factors → DensePoly.Monic g) (hproduct_mod_p : (List.map FpPoly.liftToZ factors).toArray.polyProduct.congr f p) (hcoprime : QuadraticMultifactorCoprimeSplits p factors) (hnonempty : factors ≠ []) : QuadraticMultifactorLiftInvariant p k f (List.map FpPoly.liftToZ factors)

Build the recursive quadratic multifactor lift invariant from the natural mod-p boundary facts. The caller supplies, for the list of FpPoly p factors lifted via FpPoly.liftToZ:

• hf_monic and hfactors_monic; f and every factor is monic (each split's leading factor is monic; f itself is needed recursively as the doubling-loop's target stays monic);

• hproduct_mod_p; the lifted ordered product is congruent to f mod p (feeds the product half of QuadraticLiftLoopInvariant);

• hcoprime : QuadraticMultifactorCoprimeSplits p factors; every split's normalised XGCD has gcd = 1 over FpPoly p (feeds the Bezout half via normalizedXGCD_liftToZ_bezout_congr_of_gcd_eq_one);

• hnonempty; the factor list is nonempty (rules out the vacuous base case which would force congr 1 f (p^k)).

The recursive tail re-establishes the same package using henselLiftQuadratic_h_congr_mod_base for the lifted complementary factor and henselLiftQuadratic_h_monic for its monicness.

@[simp]

theorem Hex.ZPoly.multifactorLiftQuadratic_size_eq_input (p k : Nat) [ZMod64.Bounds p] (f : ZPoly) (factors : Array ZPoly) : (multifactorLiftQuadratic p k f factors).size = factors.size

The multifactorLiftQuadratic output has one entry per input factor. Used by the Mathlib-side injectivity wrapper to relate output array indices to original modular-factor indices.

@[simp]

theorem Hex.ZPoly.multifactorLiftQuadratic_empty (p k : Nat) [ZMod64.Bounds p] (f : ZPoly) : multifactorLiftQuadratic p k f #[] = #[]

The empty-input boundary of multifactorLiftQuadratic: no factors in, no factors out.

@[simp]

theorem Hex.ZPoly.multifactorLiftQuadratic_singleton (p k : Nat) [ZMod64.Bounds p] (f g : ZPoly) : multifactorLiftQuadratic p k f #[g] = #[f.reduceModPow p k]

The singleton-input boundary of multifactorLiftQuadratic: a single factor input collapses to the target polynomial reduced modulo p^k. The input factor is discarded because the only remaining lift target is f itself under the trivial split f = f * 1.

theorem Hex.ZPoly.multifactorLiftQuadratic_each_congr_mod_base (p k : Nat) [ZMod64.Bounds p] (f : ZPoly) (factors : Array ZPoly) (hk : 1 ≤ k) (hp : 1 < p) (hf_monic : DensePoly.Monic f) (hfactors_monic : ∀ (g : ZPoly), g ∈ factors → DensePoly.Monic g) (hinv : QuadraticMultifactorLiftInvariant p k f factors.toList) (hproduct : factors.polyProduct.congr f p) (i : Nat) : ((multifactorLiftQuadratic p k f factors).toList[i]?.getD 0).congr (factors.toList[i]?.getD 0) p

Each output of multifactorLiftQuadratic is congruent modulo p to the corresponding input factor, given the monic / lift-invariant / mod-p product hypotheses of quadraticMultifactorLiftInvariant_of_factorsModP.

This is the per-output mod-p preservation surface consumed by the Mathlib theorem henselLiftData_liftedFactor_injective: pairing it with Nodup of the original modular factor list shows distinct lifted factors remain distinct as integer polynomials.

The size equality multifactorLiftQuadratic_size_eq_input is the companion fact relating output array indices to input array indices.

theorem Hex.ZPoly.multifactorLiftQuadratic_each_monic (p k : Nat) [ZMod64.Bounds p] (f : ZPoly) (factors : Array ZPoly) (hk : 1 ≤ k) (hp : 1 < p) (hf_monic : DensePoly.Monic f) (hinv : QuadraticMultifactorLiftInvariant p k f factors.toList) (i : Fin (multifactorLiftQuadratic p k f factors).size) : DensePoly.Monic (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.