theorem HexBerlekampZassenhausMathlib.IntReductionMod.normalizeForFactor_repeatedPart_map_intCast_dvd_squareFreeCore_map_intCast_pow (f : Hex.ZPoly) (hf : f ≠ 0) : ∃ (N : ℕ), Polynomial.map (Int.castRingHom ℚ) (HexPolyZMathlib.toPolynomial (Hex.normalizeForFactor f).repeatedPart) ∣ Polynomial.map (Int.castRingHom ℚ) (HexPolyZMathlib.toPolynomial (Hex.normalizeForFactor f).squareFreeCore) ^ N

Specialisation of the abstract rp_dvd_sf_pow_of_associated step to the executable normalizeForFactor surface, transported to Polynomial ℚ via HexPolyZMathlib.toPolynomial and Polynomial.map (Int.castRingHom ℚ).

This is the rational-side divisibility theorem consumed by the integer Gauss descent and exponent extraction.

theorem HexBerlekampZassenhausMathlib.IntReductionMod.normalizeForFactor_repeatedPart_toPolynomial_dvd_squareFreeCore_pow (f : Hex.ZPoly) (hf : f ≠ 0) : ∃ (N : ℕ), HexPolyZMathlib.toPolynomial (Hex.normalizeForFactor f).repeatedPart ∣ HexPolyZMathlib.toPolynomial (Hex.normalizeForFactor f).squareFreeCore ^ N

The repeated part of normalizeForFactor f divides a power of the primitive square-free part over integer polynomials.

This is the integer Gauss-descent form of normalizeForFactor_repeatedPart_map_intCast_dvd_squareFreeCore_map_intCast_pow.

theorem HexBerlekampZassenhausMathlib.IntReductionMod.normalizeForFactor_repeatedPart_normalizedFactor_covered_by_coreFactors (f : Hex.ZPoly) (hf : f ≠ 0) (coreFactors : Array Hex.ZPoly) (hirr : ∀ q ∈ coreFactors.toList, q.Irreducible) (hprod : coreFactors.polyProduct = (Hex.normalizeForFactor f).squareFreeCore) (r : Polynomial ℤ) : r ∈ UniqueFactorizationMonoid.normalizedFactors (HexPolyZMathlib.toPolynomial (Hex.normalizeForFactor f).repeatedPart) → ∃ q ∈ coreFactors.toList, Associated r (HexPolyZMathlib.toPolynomial q)

Every normalized irreducible factor of the repeated part is represented, up to association in Polynomial ℤ, by one of the supplied irreducible factors of the square-free part.

This is the normalized-factor support step consumed by the successor exponent-list construction for normalizeForFactor_repeatedPart_isPow_polyProduct_of_irreducible_factors_cover. It combines the repeated-part power-divisibility theorem with the polyProduct_toPolynomial identification for the supplied coreFactors.

theorem HexBerlekampZassenhausMathlib.IntReductionMod.toPolynomial_factorPower_foldl (entries : List (Hex.ZPoly × ℕ)) : HexPolyZMathlib.toPolynomial (List.foldl (fun (x1 x2 : Hex.ZPoly) => x1 * x2) 1 (List.map (fun (qe : Hex.ZPoly × ℕ) => Hex.Factorization.factorPower qe.1 qe.2) entries)) = (List.map (fun (qe : Hex.ZPoly × ℕ) => HexPolyZMathlib.toPolynomial qe.1 ^ qe.2) entries).prod

The ordered executable product of public Hex.Factorization.factorPower entries agrees with the ordered Polynomial ℤ product of transported powers.

This is the product lemma consumed by repeated-part exponent decompositions before invoking the Mathlib-free expansion helper.

theorem HexBerlekampZassenhausMathlib.IntReductionMod.normalizeForFactor_repeatedPart_isPow_polyProduct_of_irreducible_factors_cover (f : Hex.ZPoly) (_hf : f ≠ 0) (coreFactors : Array Hex.ZPoly) (_hirr : ∀ q ∈ coreFactors.toList, q.Irreducible) (_hprod : coreFactors.polyProduct = (Hex.normalizeForFactor f).squareFreeCore) (exponents : List ℕ) (hlen : exponents.length = coreFactors.size) (hpoly_decomp : HexPolyZMathlib.toPolynomial (Hex.normalizeForFactor f).repeatedPart = (List.map (fun (qe : Hex.ZPoly × ℕ) => HexPolyZMathlib.toPolynomial qe.1 ^ qe.2) (coreFactors.toList.zip exponents)).prod) : ∃ (exponents : List ℕ), exponents.length = coreFactors.size ∧ (Hex.normalizeForFactor f).repeatedPart = List.foldl (fun (x1 x2 : Hex.ZPoly) => x1 * x2) 1 (List.map (fun (qe : Hex.ZPoly × ℕ) => Hex.Factorization.factorPower qe.1 qe.2) (coreFactors.toList.zip exponents))

Polynomial-to-executable lemma for the repeated-part power decomposition.

The remaining mathematical side condition is the polynomial-level exact decomposition hpoly_decomp. The normalized-factor exponent extraction shows that every normalized factor of the repeated part occurs among the supplied factors of the square-free part; the caller must still show that the chosen exponents multiply to the transported repeated part. This theorem then converts that certificate into the exact executable Factorization.factorPower fold consumed by Hex.expandRepeatedPartFactorArray_residual_eq_one_of_pow_decomposition.

theorem HexBerlekampZassenhausMathlib.IntReductionMod.normalizeForFactor_repeatedPart_isFactorPower_polyProduct_of_irreducible_factors_cover (f : Hex.ZPoly) (hf : f ≠ 0) (coreFactors : Array Hex.ZPoly) (hirr : ∀ q ∈ coreFactors.toList, q.Irreducible) (hprod : coreFactors.polyProduct = (Hex.normalizeForFactor f).squareFreeCore) (hnorm : ∀ q ∈ coreFactors.toList, Hex.normalizeFactorSign q = q) : ∃ (exponents : List ℕ), exponents.length = coreFactors.size ∧ (Hex.normalizeForFactor f).repeatedPart = List.foldl (fun (x1 x2 : Hex.ZPoly) => x1 * x2) 1 (List.map (fun (qe : Hex.ZPoly × ℕ) => Hex.Factorization.factorPower qe.1 qe.2) (coreFactors.toList.zip exponents))

Every irreducible cover of (Hex.normalizeForFactor f).squareFreeCore lifts to an exponent list whose Hex.Factorization.factorPower-fold reconstructs (Hex.normalizeForFactor f).repeatedPart in Hex.ZPoly. This is the form consumed by the public Mathlib-free expansion wrapper Hex.expandRepeatedPartFactorArray_residual_eq_one_of_factorPower_decomposition.

The proof composes three structural lemmas:

• normalizeForFactor_repeatedPart_normalizedFactor_covered_by_coreFactors, which guarantees every normalized factor of the repeated part is associated to one of the supplied factors of the square-free part;

• the normalize identifications normalizeForFactor_repeatedPart_toPolynomial_normalize and HexBerlekampZassenhausMathlib.normalize_toPolynomial_of_normalizeFactorSign_id, which align the repeated part and each supplied square-free factor with the normalize-fixed UFD canonical form in Polynomial ℤ;

• normalizeForFactor_squareFreeCore_toPolynomial_squarefree, which (via the local List.nodup_of_prod_squarefree helper) makes the transported square-free-factor list pairwise distinct so that exponents per position are unambiguous, and Mathlib's Finset.prod_multiset_count_of_subset re-expresses (normalizedFactors R).prod as a finset-product over the list's toFinset.

The constructed exponents are exponents[i] = Multiset.count (toPolynomial coreFactors[i]) (normalizedFactors R) where R = toPolynomial (normalizeForFactor f).repeatedPart.

The hnorm hypothesis (Hex.normalizeFactorSign q = q for each supplied square-free part factor) is downstream-friendly: every arm discharger reaches this point after multifactorLiftQuadratic, where the lifted factors are monic, so normalizeFactorSign q = q is immediate from monicity (leadingCoeff = 1).

theorem HexBerlekampZassenhausMathlib.IntReductionMod.factorPower_cover_not_dvd_tail_of_irreducible_squarefree (f : Hex.ZPoly) (hf : f ≠ 0) (coreFactors : Array Hex.ZPoly) (hirr : ∀ q ∈ coreFactors.toList, q.Irreducible) (hprod : coreFactors.polyProduct = (Hex.normalizeForFactor f).squareFreeCore) (hnorm : ∀ q ∈ coreFactors.toList, Hex.normalizeFactorSign q = q) (exponents : List ℕ) (hlen : exponents.length = coreFactors.size) (pre : List (Hex.ZPoly × ℕ)) (q : Hex.ZPoly) (e : ℕ) (suf : List (Hex.ZPoly × ℕ)) : coreFactors.toList.zip exponents = pre ++ (q, e) :: suf → ¬q ∣ List.foldl (fun (x1 x2 : Hex.ZPoly) => x1 * x2) 1 (List.map (fun (qe : Hex.ZPoly × ℕ) => Hex.Factorization.factorPower qe.1 qe.2) suf)

Given an irreducible cover coreFactors of (Hex.normalizeForFactor f).squareFreeCore and any exponent list of matching length, splitting the zipped list coreFactors.toList.zip exponents at any position (pre, (q, e), suf) yields a suffix whose factorPower-fold product is not divisible by q.

This is the list-shaped generalisation of Hex.irreducible_not_dvd_one (which handles the singleton-suffix case where the product collapses to 1) and is the precondition consumed by the exhaustive arm of Hex.expandRepeatedPartFactorArray_residual_eq_one_of_factorPower_decomposition.

The proof transports both q and the suffix product to Polynomial ℤ through HexPolyZMathlib.equiv, uses the primitive square-free part to obtain Nodup of the transported square-free-factor list, and finishes with a UFD prime-divides-product argument: toPolynomial q is prime in Polynomial ℤ, so any divisor witness would force q to coincide with some entry in suf (by Associated ⟹ normalize-fixed equality, then injectivity), contradicting Nodup.

theorem HexBerlekampZassenhausMathlib.IntReductionMod.reassemblyExpansionComplete_of_irreducible_squarefree_cover (f : Hex.ZPoly) (hf : f ≠ 0) (coreFactors : Array Hex.ZPoly) (hirr : ∀ q ∈ coreFactors.toList, q.Irreducible) (hprod : coreFactors.polyProduct = (Hex.normalizeForFactor f).squareFreeCore) (hnorm : ∀ q ∈ coreFactors.toList, Hex.normalizeFactorSign q = q) (hmonic : ∀ q ∈ coreFactors.toList, Hex.DensePoly.Monic q) (hdegree : ∀ q ∈ coreFactors.toList, 0 < Hex.DensePoly.natDegree q) (hfuel : ∀ (exponents : List ℕ), exponents.length = coreFactors.size → (Hex.normalizeForFactor f).repeatedPart = List.foldl (fun (x1 x2 : Hex.ZPoly) => x1 * x2) 1 (List.map (fun (qe : Hex.ZPoly × ℕ) => Hex.Factorization.factorPower qe.1 qe.2) (coreFactors.toList.zip exponents)) → ∀ qe ∈ coreFactors.toList.zip exponents, qe.2 + 1 ≤ Hex.DensePoly.size (Hex.normalizeForFactor f).repeatedPart + 1) : Hex.reassemblyExpansionComplete (Hex.normalizeForFactor f) coreFactors

Assemble expansion completeness from an irreducible square-free cover.

Given an irreducible factor cover of (Hex.normalizeForFactor f).squareFreeCore, the repeated-part factorPower decomposition from normalizeForFactor_repeatedPart_isFactorPower_polyProduct_of_irreducible_factors_cover and the no-tail-divisibility theorem factorPower_cover_not_dvd_tail_of_irreducible_squarefree supply the two semantic hypotheses of the executable expansion helper.

The remaining hmonic, hdegree, and hfuel hypotheses are executable compatibility shims required by Hex.expandRepeatedPartFactorArray_residual_eq_one_of_factorPower_decomposition. They are intentionally explicit here so branch-specific callers can discharge or thread them without hiding another analytic obligation.

theorem HexBerlekampZassenhausMathlib.IntReductionMod.reassemblyExpansionComplete_of_irreducible_squarefree_cover_of_pos_lc (f : Hex.ZPoly) (hf : f ≠ 0) (coreFactors : Array Hex.ZPoly) (hirr : ∀ q ∈ coreFactors.toList, q.Irreducible) (hprod : coreFactors.polyProduct = (Hex.normalizeForFactor f).squareFreeCore) (hnorm : ∀ q ∈ coreFactors.toList, Hex.normalizeFactorSign q = q) (hpos_lc : ∀ q ∈ coreFactors.toList, 0 < Hex.DensePoly.leadingCoeff q) (hdegree : ∀ q ∈ coreFactors.toList, 0 < Hex.DensePoly.natDegree q) (hfuel : ∀ (exponents : List ℕ), exponents.length = coreFactors.size → (Hex.normalizeForFactor f).repeatedPart = List.foldl (fun (x1 x2 : Hex.ZPoly) => x1 * x2) 1 (List.map (fun (qe : Hex.ZPoly × ℕ) => Hex.Factorization.factorPower qe.1 qe.2) (coreFactors.toList.zip exponents)) → ∀ qe ∈ coreFactors.toList.zip exponents, qe.2 + 1 ≤ Hex.DensePoly.size (Hex.normalizeForFactor f).repeatedPart + 1) : Hex.reassemblyExpansionComplete (Hex.normalizeForFactor f) coreFactors

Non-monic _of_pos_lc sibling of reassemblyExpansionComplete_of_irreducible_squarefree_cover: replaces the per-factor Monic q premise with 0 < leadingCoeff q, delegating to Hex.expandRepeatedPartFactorArray_residual_eq_one_of_factorPower_decomposition_of_pos_lc from HexBerlekampZassenhaus. This provides a surface for callers wanting to delegate to the assembler under a primitive + pos-lc precondition; the existing quadratic-arm caller reassemblyExpansionComplete_quadraticIntegerRootFactors_of_ne_zero (below) bypasses this theorem by handling through the leaf directly, while reassemblyExpansionComplete_exhaustive_of_ne_zero uses this variant.

theorem HexBerlekampZassenhausMathlib.IntReductionMod.reassemblyExpansionComplete_of_irreducible_squarefree_cover_of_norm (f : Hex.ZPoly) (hf : f ≠ 0) (coreFactors : Array Hex.ZPoly) (hirr : ∀ q ∈ coreFactors.toList, q.Irreducible) (hprod : coreFactors.polyProduct = (Hex.normalizeForFactor f).squareFreeCore) (hnorm : ∀ q ∈ coreFactors.toList, Hex.normalizeFactorSign q = q) (hdegree : ∀ q ∈ coreFactors.toList, 0 < Hex.DensePoly.natDegree q) : Hex.reassemblyExpansionComplete (Hex.normalizeForFactor f) coreFactors

Sign-normalized sibling of reassemblyExpansionComplete_of_irreducible_squarefree_cover_of_pos_lc: derives the per-factor positive leading coefficient from the sign-normalization identity plus irreducibility (hence nonzero-ness), and the fuel bound from the per-factor factorPower size lower bound together with size_le_of_dvd_nonzero, so callers supply only the irreducible, sign-normalized, positive-degree cover of the primitive square-free part. Consumed by the classical residual arm (reassemblyExpansionComplete_classicalCore_of_ne_zero) and the lattice method (reassemblyExpansionComplete_latticeCore_of_ne_zero, LatticeFactorization.lean).

theorem HexBerlekampZassenhausMathlib.IntReductionMod.normalizeForFactor_repeatedPart_isFactorPower_squareFreeCore_of_irreducible (f : Hex.ZPoly) (hf : f ≠ 0) (hirr : (Hex.normalizeForFactor f).squareFreeCore.Irreducible) : ∃ (k : ℕ), (Hex.normalizeForFactor f).repeatedPart = Hex.Factorization.factorPower (Hex.normalizeForFactor f).squareFreeCore k

Small-mod singleton factorPower shape of the repeated part. Singleton specialisation of normalizeForFactor_repeatedPart_isFactorPower_polyProduct_of_irreducible_factors_cover: when the normalized primitive square-free part is itself irreducible, the repeated part is exactly a Hex.Factorization.factorPower of the primitive square-free part. The hnorm precondition of the general theorem is discharged by Hex.squareFreeCore_normalizeFactorSign_of_ne_zero (the normalized primitive square-free part has positive leading coefficient, hence its sign-normalisation is the identity). It is consumed by Hex.reassemblyExpansionComplete_singleton_of_irreducible to selection the singleton expansion theorem Hex.expandRepeatedPartFactorArray_pow_singleton.

theorem HexBerlekampZassenhausMathlib.IntReductionMod.reassemblyExpansionComplete_singleton_of_irreducible (f : Hex.ZPoly) (hf : f ≠ 0) (hirr : (Hex.normalizeForFactor f).squareFreeCore.Irreducible) (hmonic : Hex.DensePoly.Monic (Hex.normalizeForFactor f).squareFreeCore) (hdeg : 0 < Hex.DensePoly.natDegree (Hex.normalizeForFactor f).squareFreeCore) : Hex.reassemblyExpansionComplete (Hex.normalizeForFactor f) #[(Hex.normalizeForFactor f).squareFreeCore]

Small-mod singleton reassembly completeness. When the normalized primitive square-free part is itself irreducible, the singleton-part reassembly is expansion-complete: the repeatedPart of normalizeForFactor f is exactly a Hex.Factorization.factorPower of the primitive square-free part, and that factorPower is consumed completely by Hex.expandRepeatedPartFactorArray. It lets singleton-part callers derive expansion completeness from irreducibility instead of carrying it as a separate premise.

The explicit hmonic premise is required because the executable extraction (consumeExactPower_pow_mul_of_not_dvd and the expandRepeatedPartFactorArray_residual_eq_one_of_factorPower_decomposition wrapper) currently requires monicness of the square-free factor; dropping the hypothesis would require a non-monic divMod/exactQuotient generalisation in HexPolyZ/Basic.lean.

theorem HexBerlekampZassenhausMathlib.IntReductionMod.reassemblyExpansionComplete_quadraticIntegerRootFactors_of_ne_zero (f : Hex.ZPoly) (hf : f ≠ 0) {coreFactors : Array Hex.ZPoly} (hquad : Hex.quadraticIntegerRootFactors? (Hex.normalizeForFactor f).squareFreeCore = some coreFactors) : Hex.reassemblyExpansionComplete (Hex.normalizeForFactor f) coreFactors

Discharge reassembly expansion for the quadratic integer-root branch. When the normalized primitive square-free part (normalizeForFactor f).squareFreeCore factors through the executable quadraticIntegerRootFactors? short-circuit (returning some coreFactors), the reassembly of the recorded factors of the square-free part is expansion-complete: the repeatedPart of normalizeForFactor f is exactly the Factorization.factorPower foldl product over the square-free-factor / exponent pairs supplied by normalizeForFactor_repeatedPart_isFactorPower_polyProduct_of_irreducible_factors_cover, and that fold is consumed completely by Hex.expandRepeatedPartFactorArray. Consumed by the slow-path and fast-path quadratic arm umbrellas (factor_quadratic_branch_entry_irreducible_of_quadraticRoots and factor_slow_quadratic_branch_entry_irreducible_of_choosePrimeData) so their callers can drop the explicit hcomplete premise on the quadratic arms.

Composes:

• Hex.squareFreeCore_leadingCoeff_pos_of_ne_zero and the Mathlib-side lemma zpoly_primitive_of_toPolynomial_isPrimitive ∘ normalizeForFactor_squareFreeCore_toPolynomial_isPrimitive; the squareFreeCore positive-leading-coefficient and primitivity invariants;

• Hex.quadraticIntegerRootFactors?_factor_irreducible_of_primitive; every emitted square-free factor is irreducible under primitivity;

• Hex.polyProduct_quadraticIntegerRootFactors?_some; the polyProduct = squareFreeCore invariant;

• Hex.quadraticIntegerRootFactors?_normalizeFactorSign; the per-factor normalizeFactorSign identity, discharging the hnorm precondition of normalizeForFactor_repeatedPart_isFactorPower_polyProduct_of_irreducible_factors_cover;

• Hex.quadraticIntegerRootFactors?_factor_size_eq_two; every square-free factor has dense size two, supplying the per-factor positive leading coefficient and positive degree preconditions of the non-monic expansion-complete surface;

• normalizeForFactor_repeatedPart_isFactorPower_polyProduct_of_irreducible_factors_cover ; the structural factorPower decomposition of the repeated part;

• factorPower_cover_not_dvd_tail_of_irreducible_squarefree; the per-position tail-non-divisibility certificate;

• Hex.expandRepeatedPartFactorArray_residual_eq_one_of_factorPower_decomposition_of_pos_lc ; the non-monic public expansion-complete surface; the non-monic version is required because quadraticIntegerRootFactors? may emit a primitive non-monic residual (e.g. 2X + 3 from (X-1)(2X+3) = 2X^2 + X - 3).

The corresponding constant, small-mod singleton, and exhaustive branch theorems are Hex.reassemblyExpansionComplete_constant_of_ne_zero, reassemblyExpansionComplete_singleton_of_irreducible, and reassemblyExpansionComplete_exhaustive_of_ne_zero.