theorem HexBerlekampZassenhausMathlib.quadraticMultifactorCoprimeSplits_of_factorProduct_no_squared {p : ℕ} [Hex.ZMod64.Bounds p] [Hex.ZMod64.PrimeModulus p] [Lean.Grind.Field (Hex.ZMod64 p)] (X : Hex.FpPoly p) (hX_ne : X ≠ 0) (h_no_squared : ∀ (d : Hex.FpPoly p), d * d ∣ X → ¬0 < Hex.DensePoly.natDegree d) (xs : List (Hex.FpPoly p)) (h_dvd : Hex.Berlekamp.factorProduct xs ∣ X) : Hex.ZPoly.QuadraticMultifactorCoprimeSplits p xs

Generalized inductive helper for the factorsModP_coprime discharger.

For any list of factors in FpPoly p whose factorProduct divides a nonzero polynomial X with no positive-degree squared divisor, the recursive predicate Hex.ZPoly.QuadraticMultifactorCoprimeSplits holds.

The recursion follows the guarded product tree: at each non-singleton node the list splits into L := take split and R := drop split, using the same balancedSplitIndex as the executable, and

• xgcd.gcd = 1 follows from the coprime view of factorProduct L against factorProduct R, identified via modP_polyProduct_liftToZ_eq_factorProduct: their DensePoly.gcd squares into factorProduct (L ++ R) = factorProduct xs, hence into X, so the no-squared invariant forces it constant;

• each side satisfies the same divisibility-into-X invariant via factorProduct L ∣ factorProduct xs ∣ X (and symmetrically for R), using factorProduct_append.

theorem HexBerlekampZassenhausMathlib.factorsModP_coprime_of_factorsModPBerlekampForm (core : Hex.ZPoly) (primeData : Hex.PrimeChoiceData) (hform : Hex.factorsModPBerlekampForm core primeData) (hgood : Hex.isGoodPrime core primeData.p = true) : Hex.ZPoly.QuadraticMultifactorCoprimeSplits primeData.p primeData.factorsModP.toList

Discharge of the coprime-splits boundary premise on Hex.ZPoly.QuadraticMultifactorLiftInvariant_of_choosePrimeData: 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, the recursive balanced-split coprime predicate QuadraticMultifactorCoprimeSplits holds on the stored factor list.

Proof: extract the Berlekamp witnesses from hform; transport modular squarefreeness from isGoodPrime through monicModularImage; apply the generalized quadraticMultifactorCoprimeSplits_of_factorProduct_no_squared helper with X := monicModularImage (modP p core) to walk the list. The no-squared invariant on the modular image is the local Mathlib-side form of gcd_monicModularImage_derivative_isUnit_local, instantiated through Hex.Berlekamp.isUnitPolynomial_of_squareFree_of_squared_dvd.

This is the third in the chain of factorsModP-side dischargers (factorsModP_nodup_of_factorsModPBerlekampForm, factorsModP_natDegree_pos_of_factorsModPBerlekampForm, this one), each mapping the abstract factorsModPBerlekampForm invariant plus an isGoodPrime certificate to a piece of the four-tuple (hfactors_monic, hproduct_mod_p, hcoprime, hnonempty) that the umbrella QuadraticMultifactorLiftInvariant_of_choosePrimeData consumes.

The Option-3 wrap of berlekampFactorsModP (apply monicModularImage per factor) lifts the helper application from the raw Berlekamp factor list to the mapped list via the multiplicativity lemma factorProduct_map_monicModularImage_eq_monicModularImage_factorProduct.

theorem HexBerlekampZassenhausMathlib.factorsModP_monic_of_factorsModPBerlekampForm (core : Hex.ZPoly) (primeData : Hex.PrimeChoiceData) (hform : Hex.factorsModPBerlekampForm core primeData) (g : Hex.FpPoly primeData.p) : g ∈ primeData.factorsModP → Hex.DensePoly.Monic g

Discharge of the per-modular-factor monicness premise on henselLiftData_liftedFactor_monic_of_choosePrimeData (and the two other umbrellas at lines 5136 and 5200) from the factorsModPBerlekampForm invariant alone.

primeData.factorsModP is, under the Option-3 wrap in berlekampFactorsModP, exactly ((berlekampFactor monicImg).factors.map monicModularImage).toArray. Every entry is therefore the monicModularImage of some raw Berlekamp factor, which is monic by monicModularImage_monic provided the raw factor is nonzero. The raw-factor nonzeroness is berlekampFactor_factors_ne_zero (positive-degree case via berlekampFactor_factors_pos_degree, degenerate [monicImg] case because monicImg is monic).

No hgood or hcore_monic premise is needed: the discharge follows from the shape of factorsModPBerlekampForm and Berlekamp-output structural facts alone. This is the fourth and last of the QuadraticMultifactorLiftInvariant boundary dischargers (together with factorsModP_ne_nil_*, factorsModP_polyProduct_congr_*, and factorsModP_coprime_*) that the umbrellas consume via QuadraticMultifactorLiftInvariant_of_choosePrimeData.

theorem HexBerlekampZassenhausMathlib.factors_irreducible_of_factorsModPBerlekampForm (core : Hex.ZPoly) (primeData : Hex.PrimeChoiceData) (hform : Hex.factorsModPBerlekampForm core primeData) (hgood : Hex.isGoodPrime core primeData.p = true) (hcore_pos : 0 < Hex.DensePoly.natDegree core) (i : ModPFactorIndex primeData) : Irreducible (HexPolyFpMathlib.toMathlibPolynomial (modPFactor primeData i))

factorsModPBerlekampForm-shaped discharge for per-modular-factor irreducibility after the Mathlib-side transport.

Given the factorsModPBerlekampForm invariant (recording that primeData.factorsModP is the post-monicModularImage 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 transported Mathlib polynomial of every stored modular factor is irreducible.

Proof: each entry of primeData.factorsModP is monicModularImage g for some raw Berlekamp factor g. irreducible_of_mem_berlekampFactor gives Irreducible (toMathlibPolynomial g). The transfer to monicModularImage g uses toMathlibPolynomial_scale: since monicModularImage g = scale (lc g)⁻¹ g, the Mathlib image equals C ((lc g)⁻¹.toZMod) * toMathlibPolynomial g, a unit multiple of the original, and Associated.irreducible transfers the irreducibility.

The square-freeness premise of irreducible_of_mem_berlekampFactor is discharged via gcd_monicModularImage_derivative_isUnit_local applied to the modular square-freeness from Hex.isGoodPrime_squareFreeModP.

This is the per-index irreducibility component consumed by the ModPSubsetPartitionHypotheses constructor. The sibling existence / uniqueness component is existsUnique_modPFactorSubset_of_choosePrimeData; the constructor wrapper itself is modPSubsetPartitionHypotheses_of_choosePrimeData.

theorem HexBerlekampZassenhausMathlib.factors_irreducible_of_choosePrimeData_of_some (core : Hex.ZPoly) (primeData : Hex.PrimeChoiceData) (hselected : Hex.choosePrimeData? core = some primeData) (hcore_pos : 0 < Hex.DensePoly.natDegree core) (i : ModPFactorIndex primeData) : Irreducible (HexPolyFpMathlib.toMathlibPolynomial (modPFactor primeData i))

Per-modular-factor irreducibility specialised to the Hex.choosePrimeData? core = some primeData branch.

In this branch, the factorsModPBerlekampForm invariant and the isGoodPrime hypothesis are both supplied automatically by Hex.choosePrimeData?_factorsModP_berlekamp_form and Hex.choosePrimeData?_isGoodPrime respectively; the none branch is excluded by the explicit-witness premise hselected. The constructor wrapper will compose this with the sibling existsUnique_modPFactorSubset_of_choosePrimeData and the trivial fModP_eq / admissible_prime / square_free_reduction fields.