theorem HexBerlekampZassenhausMathlib.henselLiftData_liftedFactor_modP_eq_modPFactor (core : Hex.ZPoly) (B : ℕ) (primeData : Hex.PrimeChoiceData) (hcore_monic : Hex.DensePoly.Monic core) (hprime_invariant : Hex.ZPoly.QuadraticMultifactorLiftInvariant primeData.p B core (Array.map Hex.FpPoly.liftToZ primeData.factorsModP).toList) (hp : 1 < primeData.p) (hB : 1 ≤ B) (hfactors_monic : ∀ g ∈ primeData.factorsModP, Hex.DensePoly.Monic g) (hproduct_mod_p : (Array.map Hex.FpPoly.liftToZ primeData.factorsModP).polyProduct.congr core primeData.p) (i : ModPFactorIndex primeData) : Hex.ZPoly.modP primeData.p (liftedFactor (Hex.henselLiftData core B primeData) (liftedIndexOfModPIndex primeData (Hex.henselLiftData core B primeData) ⋯ i)) = modPFactor primeData i

Each lifted factor produced by Hex.henselLiftData reduces modulo the base prime to the corresponding modular factor selected by PrimeChoiceData.

This is a direct indexed form of Hex.ZPoly.multifactorLiftQuadratic_each_congr_mod_base, specialised to the Hex.henselLiftData umbrella and the liftedIndexOfModPIndex transport.

theorem HexBerlekampZassenhausMathlib.squareFree_common_of_squareFreeModP {p : ℕ} [Hex.ZMod64.Bounds p] [Hex.ZMod64.PrimeModulus p] (f : Hex.ZPoly) (hsf : Hex.squareFreeModP f p) (d : Hex.FpPoly p) : d ∣ Hex.ZPoly.modP p f → d ∣ Hex.DensePoly.derivative (Hex.ZPoly.modP p f) → Hex.Berlekamp.isUnitPolynomial d = true

Square-free reduction forbids a positive-degree common divisor of the image and its derivative.

theorem HexBerlekampZassenhausMathlib.factorsModP_nodup_of_factorsModPBerlekampForm (f : Hex.ZPoly) (data : Hex.PrimeChoiceData) (hform : Hex.factorsModPBerlekampForm f data) (hgood : Hex.isGoodPrime f data.p = true) : data.factorsModP.toList.Nodup

choosePrimeData-shaped caller wrapper for the Berlekamp factor Nodup property: given the factorsModPBerlekampForm invariant (which records that primeData.factorsModP is the Berlekamp factor array of the monic modular image of the input) together with a successful isGoodPrime check (which certifies the modular image is square-free), the stored factor list has no duplicates.

Proof: extract the existential witnesses from factorsModPBerlekampForm to view data.factorsModP.toList as the Berlekamp factor list of monicModularImage (modP data.p f), then apply the polymorphic abstract loop invariant Hex.Berlekamp.berlekampFactor_factors_nodup_of_no_squared. The squareness-free hypothesis is discharged by transferring any g * g divisor through monicModularImage modP_f ∣ modP_f (via Hex.FpPoly.dvd_scale_self_of_ne_zero) and applying Hex.Berlekamp.isUnitPolynomial_of_squareFree_of_squared_dvd to the modular squarefreeness obtained from Hex.isGoodPrime_squareFreeModP.

This is the wrapper that lets a Mathlib-side caller of henselLiftData_liftedFactor_injective_of_choosePrimeData (below) discharge the hfactorsModP_nodup parameter from the choosePrimeData? facts alone, without constructing the Berlekamp Nodup argument by hand.

theorem HexBerlekampZassenhausMathlib.monicModularImage_modP_degree?_pos_of_factorsModPBerlekampForm (f : Hex.ZPoly) (data : Hex.PrimeChoiceData) (hform : Hex.factorsModPBerlekampForm f data) (hgood : Hex.isGoodPrime f data.p = true) (hf_pos : 0 < Hex.DensePoly.natDegree f) : 0 < Hex.DensePoly.natDegree (Hex.monicModularImage (Hex.ZPoly.modP data.p f))

Under the factorsModPBerlekampForm invariant and a good prime, a positive- degree input polynomial has a positive-degree monic modular image. isGoodPrime's leading-coefficient admissibility preserves the degree through modP, and the monic rescale is by a nonzero unit, so it preserves size. This is the positivity guard consumed by the per-modular-factor Mathlib irreducibility correspondence.

theorem HexBerlekampZassenhausMathlib.factorsModP_natDegree_pos_of_factorsModPBerlekampForm (f : Hex.ZPoly) (data : Hex.PrimeChoiceData) (hform : Hex.factorsModPBerlekampForm f data) (hgood : Hex.isGoodPrime f data.p = true) (hf_pos : 0 < Hex.DensePoly.natDegree f) (g : Hex.FpPoly data.p) : g ∈ data.factorsModP → 0 < (HexPolyZMathlib.toPolynomial g.liftToZ).natDegree

Discharge of the per-modular-factor natural-degree positivity premise on henselLiftData_liftedFactor_natDegree_pos: given the factorsModPBerlekampForm invariant (which records that primeData.factorsModP is the Berlekamp factor array of the monic modular image of the input) together with a successful isGoodPrime check and a positive-degree input polynomial, every modular factor lifts back to a positive-natural-degree Mathlib polynomial over ℤ.

Proof: extract the existential witnesses from factorsModPBerlekampForm to view data.factorsModP as the Berlekamp factor list of monicModularImage (modP data.p f), then apply the polymorphic abstract Hex.Berlekamp.berlekampFactor_factors_pos_degree. The required positivity of the monic modular image follows from isGoodPrime's leading-coefficient admissibility (which preserves degree through modP) together with the input's positive degree. The deduction from 0 < g.natDegree on each FpPoly p factor to 0 < (toPolynomial (liftToZ g)).natDegree on the integer side is HexPolyMathlib.natDegree_toPolynomial plus the (inline) observation that liftToZ preserves size on any nonzero FpPoly p.

This is the sibling of factorsModP_nodup_of_factorsModPBerlekampForm: it lets a Mathlib-side caller of henselLiftData_liftedFactor_natDegree_pos_of_choosePrimeData discharge the hfactors_natDegree_pos premise from the choosePrimeData? facts alone, without constructing the per-modular-factor natural-degree witnesses by hand.

theorem HexBerlekampZassenhausMathlib.monicModularImage_modP_eq_of_monic {p : ℕ} [Hex.ZMod64.Bounds p] [Hex.ZMod64.PrimeModulus p] (core : Hex.ZPoly) (hcore_monic : Hex.DensePoly.Monic core) (hprime : Hex.Nat.Prime p) (hp : 1 < p) (hzero : Hex.DensePoly.isZero (Hex.ZPoly.modP p core) = false) : Hex.monicModularImage (Hex.ZPoly.modP p core) = Hex.ZPoly.modP p core

For a monic integer polynomial core and a prime modulus p > 1, the monic modular image of modP p core is just modP p core itself: the leading coefficient of the modular image is 1 (since core's is 1 and reduces to 1 mod p), so the renormalisation scaling factor is 1⁻¹ = 1.

theorem HexBerlekampZassenhausMathlib.modP_polyProduct_liftToZ_eq_factorProduct {p : ℕ} [Hex.ZMod64.Bounds p] [Hex.ZMod64.PrimeModulus p] (xs : List (Hex.FpPoly p)) : Hex.ZPoly.modP p (List.map Hex.FpPoly.liftToZ xs).toArray.polyProduct = Hex.Berlekamp.factorProduct xs

Reducing a polyProduct of canonically-lifted FpPoly p factors back modulo p recovers the in-field factorProduct. This identifies the integer-side product carried by Array.polyProduct with the FpPoly p-side product Hex.Berlekamp.factorProduct, threading the multiplicative-homomorphism property of modP through each lifted factor.

Shared base lemma for both factorsModP_polyProduct_congr_of_factorsModPBerlekampForm (via the polyProduct_map_liftToZ_congr_factorProduct corollary just below) and factorsModP_coprime_of_factorsModPBerlekampForm (which rewrites modP p (Array.polyProduct ...) to the direct factorProduct viewpoint where pairwise-coprime arguments apply).

theorem HexBerlekampZassenhausMathlib.factorsModP_polyProduct_congr_of_factorsModPBerlekampForm_of_primitive_pos_lc_core (core : Hex.ZPoly) (primeData : Hex.PrimeChoiceData) (_hcore_primitive : core.Primitive) (_hcore_lc_pos : 0 < Hex.DensePoly.leadingCoeff core) (hform : Hex.factorsModPBerlekampForm core primeData) (_hgood : Hex.isGoodPrime core primeData.p = true) : (Array.map Hex.FpPoly.liftToZ primeData.factorsModP).polyProduct.congr (Hex.monicModularImage (Hex.ZPoly.modP primeData.p core)).liftToZ primeData.p

Primitive + positive-leading-coefficient sibling of factorsModP_polyProduct_congr_of_factorsModPBerlekampForm: the Berlekamp factor product over primeData.factorsModP is congruent mod p to liftToZ (monicModularImage (modP p core)), the canonical monic representative of modP p core.

The proof mirrors the monic version up to (but not including) the monicModularImage_modP_eq_of_monic collapse: factorProduct on the raw Berlekamp factor list returns the monic input monicModularImage (modP p core) by factorProduct_berlekampFactor, factorProduct_map_monicModularImage_eq_monicModularImage_factorProduct pushes monicModularImage through the outer map, and monicModularImage_eq_self_of_monic collapses the resulting double application because monicModularImage (modP p core) is already monic (via monicModularImage_monic). The monic wrapper above adds the final monicModularImage (modP p core) = modP p core step that requires hcore_monic.

_hcore_primitive, _hcore_lc_pos, and _hgood are not consumed by the proof; they are threaded for API parity with the broader _of_primitive_pos_lc_core propagation chain.

theorem HexBerlekampZassenhausMathlib.factorsModP_polyProduct_congr_of_factorsModPBerlekampForm (core : Hex.ZPoly) (primeData : Hex.PrimeChoiceData) (hcore_monic : Hex.DensePoly.Monic core) (hform : Hex.factorsModPBerlekampForm core primeData) (hgood : Hex.isGoodPrime core primeData.p = true) : (Array.map Hex.FpPoly.liftToZ primeData.factorsModP).polyProduct.congr core primeData.p

Discharge of the polyProduct (factorsModP.map liftToZ) ≡ core (mod p) premise on henselLiftData_liftedFactor_monic_of_choosePrimeData (and the two other umbrellas at lines 4549, 4613) from the factorsModPBerlekampForm invariant plus a successful isGoodPrime check. Requires core to be monic so that the leading coefficient of modP p core is 1, hence monicModularImage (modP p core) = modP p core; under that identification the _of_primitive_pos_lc_core sibling above (which lands at liftToZ (monicModularImage (modP p core))) collapses to liftToZ (modP p core), and the lift to the integer side is closed by congr_liftToZ_modP.

The added hcore_monic premise costs downstream callers nothing: the umbrellas they feed already require it. No additional 1 < p premise is needed; it is derived from hprime's two_le.

theorem HexBerlekampZassenhausMathlib.factorsModP_ne_nil_of_factorsModPBerlekampForm (core : Hex.ZPoly) (primeData : Hex.PrimeChoiceData) (hform : Hex.factorsModPBerlekampForm core primeData) : primeData.factorsModP.toList ≠ []

Discharge of the primeData.factorsModP.toList ≠ [] premise on the lifted-factor umbrellas: the factorsModPBerlekampForm invariant records that primeData.factorsModP is exactly the Berlekamp factor array of the monic modular image, and Hex.Berlekamp.berlekampFactor_factors_ne_nil guarantees the Berlekamp factor list is nonempty for any monic input.

No hgood premise is needed: nonemptiness is preserved by berlekampFactor regardless of square-freeness, and factorsModPBerlekampForm already bundles the nonzero-image witness used to construct the monic image.

Used together with factorsModP_monic_*, factorsModP_polyProduct_congr_*, and factorsModP_coprime_* to discharge the four QuadraticMultifactorLiftInvariant boundary hypotheses fed into the umbrellas via Hex.ZPoly.QuadraticMultifactorLiftInvariant_of_choosePrimeData.