theorem Hex.quadraticIntegerRootFactors?_degree_pos_of_primitive {core : ZPoly} (hcore_pos : 0 < DensePoly.leadingCoeff core) (hcore_primitive : core.Primitive) {factors : Array ZPoly} (hquad : quadraticIntegerRootFactors? core = some factors) (factor : ZPoly) : factor ∈ factors.toList → 0 < DensePoly.natDegree factor

Every factor emitted by quadraticIntegerRootFactors? has positive degree when the input polynomial is primitive with positive leading coefficient. Linear entries are the splitter's linearFactorForRoot outputs; the optional residual cannot be constant because then its positive constant coefficient would divide the primitive polynomial's content.

theorem Hex.extractXPower_core_ne_zero_of_ne_zero (f : ZPoly) (hf : f ≠ 0) : f.primitivePart.extractXPower.core ≠ 0

Removing the maximal power of X from a nonzero primitive part leaves a nonzero factor.

theorem Hex.repeatedPart_ne_zero_of_ne_zero (f : ZPoly) (hf : f ≠ 0) : (normalizeForFactor f).repeatedPart ≠ 0

The repeated-factor part of a nonzero polynomial is nonzero.

theorem Hex.reassemblePolynomialFactors_normalizeFactorSign_of_ne_zero (f : ZPoly) (hf : f ≠ 0) (coreFactors : Array ZPoly) (hcore : ∀ (factor : ZPoly), factor ∈ coreFactors.toList → normalizeFactorSign factor = factor) (factor : ZPoly) (hmem : factor ∈ (reassemblePolynomialFactors (normalizeForFactor f) coreFactors).toList) : normalizeFactorSign factor = factor

Lift a per-factor normalize property through the reassembly: any factor appearing in reassemblePolynomialFactors is either a normalization-prefix factor (handled by polynomialNormalizationPrefixFactors_normalizeFactorSign_of_ne_zero) or appears in the supplied coreFactors.

theorem Hex.reassemblePolynomialFactors_shouldRecord_of_ne_zero (f : ZPoly) (hf : f ≠ 0) (coreFactors : Array ZPoly) (hcore : ∀ (factor : ZPoly), factor ∈ coreFactors.toList → shouldRecordPolynomialFactor factor = true) (factor : ZPoly) (hmem : factor ∈ (reassemblePolynomialFactors (normalizeForFactor f) coreFactors).toList) : shouldRecordPolynomialFactor factor = true

Lift a per-factor shouldRecord property through the reassembly.

theorem Hex.irreducible_not_dvd_of_not_associated {q₁ q₂ : ZPoly} (hq₁ : q₁.Irreducible) (hq₂ : q₂.Irreducible) (hassoc : ¬q₁.Associated q₂) : ¬q₁ ∣ q₂

Two irreducible integer polynomials that are not associated do not divide one another: if q₁ divides q₂ and both are irreducible, the irreducibility decomposition q₂ = q₁ * w forces either q₁ or w to be a unit, and the first case contradicts Irreducible q₁. Used by downstream dischargers to translate the Mathlib structural fact's "pairwise non-associate irreducible factors" condition into the direct non-divisibility hypothesis consumed by expandRepeatedPartFactorArray_residual_eq_one_of_pow_decomposition.

theorem Hex.expandRepeatedPartFactorArray_residual_eq_one_of_pow_decomposition (rp : ZPoly) (coreFactors : Array ZPoly) (hmonic : ∀ (q : ZPoly), q ∈ coreFactors.toList → DensePoly.Monic q) (hdegree : ∀ (q : ZPoly), q ∈ coreFactors.toList → 0 < DensePoly.natDegree q) (exponents : List Nat) (hlen : exponents.length = coreFactors.size) (hnot_dvd_tail : ∀ (pre : List (ZPoly × Nat)) (q : ZPoly) (e : Nat) (suf : List (ZPoly × Nat)), coreFactors.toList.zip exponents = pre ++ (q, e) :: suf → ¬q ∣ List.foldl (fun (x1 x2 : ZPoly) => x1 * x2) 1 (List.map (fun (qe : ZPoly × Nat) => Factorization.polyPow qe.fst qe.snd) suf)) (hdecomp : rp = List.foldl (fun (x1 x2 : ZPoly) => x1 * x2) 1 (List.map (fun (qe : ZPoly × Nat) => Factorization.polyPow qe.fst qe.snd) (coreFactors.toList.zip exponents))) (hfuel : ∀ (qe : ZPoly × Nat), qe ∈ coreFactors.toList.zip exponents → qe.snd + 1 ≤ DensePoly.size rp + 1) : (expandRepeatedPartFactorArray rp coreFactors).snd = 1

Array-level power-decomposition expansion helper. This is the array form of expandRepeatedPartFactorsAux_residual_eq_one_of_pow_decomposition that targets expandRepeatedPartFactorArray directly. Given a list of monic positive-degree factors of the square-free part, a matching list of exponents, a head-product decomposition rp = ∏ qᵢ ^ eᵢ, and pairwise tail-non-divisibility for each head factor relative to the suffix product, the greedy expansion completely consumes rp and reports residual 1. The downstream theorem reassemblyExpansionComplete_quadraticIntegerRootFactors_of_ne_zero supplies the Mathlib-side structural decomposition and uses this helper to conclude reassemblyExpansionComplete for quadratic inputs. The singleton theorem expandRepeatedPartFactorArray_pow_singleton specializes this shape to one irreducible factor.

theorem Hex.expandRepeatedPartFactorArray_residual_eq_one_of_factorPower_decomposition (rp : ZPoly) (coreFactors : Array ZPoly) (hmonic : ∀ (q : ZPoly), q ∈ coreFactors.toList → DensePoly.Monic q) (hdegree : ∀ (q : ZPoly), q ∈ coreFactors.toList → 0 < DensePoly.natDegree q) (exponents : List Nat) (hlen : exponents.length = coreFactors.size) (hnot_dvd_tail : ∀ (pre : List (ZPoly × Nat)) (q : ZPoly) (e : Nat) (suf : List (ZPoly × Nat)), coreFactors.toList.zip exponents = pre ++ (q, e) :: suf → ¬q ∣ List.foldl (fun (x1 x2 : ZPoly) => x1 * x2) 1 (List.map (fun (qe : ZPoly × Nat) => Factorization.factorPower qe.fst qe.snd) suf)) (hdecomp : rp = List.foldl (fun (x1 x2 : ZPoly) => x1 * x2) 1 (List.map (fun (qe : ZPoly × Nat) => Factorization.factorPower qe.fst qe.snd) (coreFactors.toList.zip exponents))) (hfuel : ∀ (qe : ZPoly × Nat), qe ∈ coreFactors.toList.zip exponents → qe.snd + 1 ≤ DensePoly.size rp + 1) : (expandRepeatedPartFactorArray rp coreFactors).snd = 1

Public factorPower spelling of expandRepeatedPartFactorArray_residual_eq_one_of_pow_decomposition.

The underlying expansion proof was developed against the private recursive power helper used by Factorization.product; downstream Mathlib-side assemblers cannot name that helper. This wrapper exposes the same contract using Factorization.factorPower, whose definition is judgmentally the same power operation and is part of the public API.

theorem Hex.expandRepeatedPartFactorArray_residual_eq_one_of_pow_decomposition_of_pos_lc (rp : ZPoly) (coreFactors : Array ZPoly) (hpos_lc : ∀ (q : ZPoly), q ∈ coreFactors.toList → 0 < DensePoly.leadingCoeff q) (hdegree : ∀ (q : ZPoly), q ∈ coreFactors.toList → 0 < DensePoly.natDegree q) (exponents : List Nat) (hlen : exponents.length = coreFactors.size) (hnot_dvd_tail : ∀ (pre : List (ZPoly × Nat)) (q : ZPoly) (e : Nat) (suf : List (ZPoly × Nat)), coreFactors.toList.zip exponents = pre ++ (q, e) :: suf → ¬q ∣ List.foldl (fun (x1 x2 : ZPoly) => x1 * x2) 1 (List.map (fun (qe : ZPoly × Nat) => Factorization.polyPow qe.fst qe.snd) suf)) (hdecomp : rp = List.foldl (fun (x1 x2 : ZPoly) => x1 * x2) 1 (List.map (fun (qe : ZPoly × Nat) => Factorization.polyPow qe.fst qe.snd) (coreFactors.toList.zip exponents))) (hfuel : ∀ (qe : ZPoly × Nat), qe ∈ coreFactors.toList.zip exponents → qe.snd + 1 ≤ DensePoly.size rp + 1) : (expandRepeatedPartFactorArray rp coreFactors).snd = 1

Non-monic analogue of expandRepeatedPartFactorArray_residual_eq_one_of_pow_decomposition: replaces the per-factor Monic q hypothesis by 0 < leadingCoeff q, delegating to the list-level non-monic helper expandRepeatedPartFactorsAux_residual_eq_one_of_pow_decomposition_of_pos_lc. Intermediate between the list-level proof and the public-API factorPower wrapper below; used by expandRepeatedPartFactorArray_residual_eq_one_of_factorPower_decomposition_of_pos_lc (the surface used by the quadratic-arm discharger reassemblyExpansionComplete_quadraticIntegerRootFactors_of_ne_zero).

theorem Hex.expandRepeatedPartFactorArray_residual_eq_one_of_factorPower_decomposition_of_pos_lc (rp : ZPoly) (coreFactors : Array ZPoly) (hpos_lc : ∀ (q : ZPoly), q ∈ coreFactors.toList → 0 < DensePoly.leadingCoeff q) (hdegree : ∀ (q : ZPoly), q ∈ coreFactors.toList → 0 < DensePoly.natDegree q) (exponents : List Nat) (hlen : exponents.length = coreFactors.size) (hnot_dvd_tail : ∀ (pre : List (ZPoly × Nat)) (q : ZPoly) (e : Nat) (suf : List (ZPoly × Nat)), coreFactors.toList.zip exponents = pre ++ (q, e) :: suf → ¬q ∣ List.foldl (fun (x1 x2 : ZPoly) => x1 * x2) 1 (List.map (fun (qe : ZPoly × Nat) => Factorization.factorPower qe.fst qe.snd) suf)) (hdecomp : rp = List.foldl (fun (x1 x2 : ZPoly) => x1 * x2) 1 (List.map (fun (qe : ZPoly × Nat) => Factorization.factorPower qe.fst qe.snd) (coreFactors.toList.zip exponents))) (hfuel : ∀ (qe : ZPoly × Nat), qe ∈ coreFactors.toList.zip exponents → qe.snd + 1 ≤ DensePoly.size rp + 1) : (expandRepeatedPartFactorArray rp coreFactors).snd = 1

Non-monic analogue of expandRepeatedPartFactorArray_residual_eq_one_of_factorPower_decomposition: replaces the per-factor Monic q hypothesis by 0 < leadingCoeff q, exposing the contract using Factorization.factorPower (the public-API power operation referenced by Mathlib-side assemblers). Consumed by the quadratic-arm discharger reassemblyExpansionComplete_quadraticIntegerRootFactors_of_ne_zero when the square-free factor emitted by quadraticIntegerRootFactors? is primitive and positive-leading but non-monic (e.g. the 2X + 3 residual from (X-1)(2X+3) = 2X^2 + X - 3).

theorem Hex.expandRepeatedPartFactorArray_pow_singleton (q : ZPoly) (k : Nat) (hq_monic : DensePoly.Monic q) (hq_degree : 0 < DensePoly.natDegree q) (hq_irr : q.Irreducible) (rp : ZPoly) (hrp : rp = Factorization.factorPower q k) (hfuel : k + 1 ≤ DensePoly.size rp + 1) : expandRepeatedPartFactorArray rp #[q] = ((List.replicate k q).toArray, 1)

Singleton expansion specialization of expandRepeatedPartFactorArray_residual_eq_one_of_factorPower_decomposition: when the repeated part rp is the k-th Hex.Factorization.factorPower of an irreducible monic positive-degree q, expanding against the singleton square-free part #[q] consumes the repeated part exactly, emitting k copies of q and reporting residual 1. It feeds the public discharger Hex.reassemblyExpansionComplete_singleton_of_irreducible; the corresponding constant-input theorem is reassemblyExpansionComplete_constant_of_ne_zero.

theorem Hex.expandRepeatedPartFactorArray_pow_singleton_of_pos_lc (q : ZPoly) (k : Nat) (hq_pos_lc : 0 < DensePoly.leadingCoeff q) (hq_degree : 0 < DensePoly.natDegree q) (hq_irr : q.Irreducible) (rp : ZPoly) (hrp : rp = Factorization.factorPower q k) (hfuel : k + 1 ≤ DensePoly.size rp + 1) : (expandRepeatedPartFactorArray rp #[q]).snd = 1

Non-monic counterpart of expandRepeatedPartFactorArray_pow_singleton: replaces the Monic q premise by 0 < leadingCoeff q, with a weakened conclusion; only the residual projection .2 = 1, not the full pair. The full-pair version has no non-monic counterpart at the executable layer (consumeExactPower_pow_mul_of_not_dvd is genuinely monic-only; under non-monic q, the recursive consumeExactPower step's quotient is not in general a power of q, even if the residual collapses to 1). The residual-only form suffices for the _of_pos_lc sibling of reassemblyExpansionComplete_singleton_of_irreducible, which unfolds reassemblyExpansionComplete to (expand ...).2 = 1. The proof uses the array-level public surface expandRepeatedPartFactorArray_residual_eq_one_of_factorPower_decomposition_of_pos_lc specialised to coreFactors = #[q], exponents = [k].

theorem Hex.squareFreeCore_leadingCoeff_pos_of_ne_zero (f : ZPoly) (hf : f ≠ 0) : 0 < DensePoly.leadingCoeff (normalizeForFactor f).squareFreeCore

The square-free part of a nonzero normalized input has positive leading coefficient.

theorem Hex.squareFreeCore_coeff_zero_ne_zero (f : ZPoly) (hf : f ≠ 0) : DensePoly.coeff (normalizeForFactor f).squareFreeCore 0 ≠ 0

The reachable primitive square-free part has a nonzero constant term. normalizeForFactor strips the visible power of X (via extractXPower) before primitiveSquareFreeDecomposition, so the square-free part fed to the prime/lift computation is not divisible by X. Over ℚ the primitive part reassembles as a unit scalar times squareFreeCore * repeatedPart; reading the constant term forces squareFreeCore.coeff 0 ≠ 0.

theorem Hex.squareFreeCore_primitive_of_ne_zero (f : ZPoly) (hf : f ≠ 0) : (normalizeForFactor f).squareFreeCore.Primitive

The normalized primitive square-free part is primitive whenever the input is nonzero. Discharges the ZPoly.Primitive core precondition of exhaustiveIntegerTrialCoreFactorsWithBound_factor_irreducible (:13443) and quadraticIntegerRootFactors?_factor_irreducible_of_primitive (:14060) when both are specialised to (normalizeForFactor f).squareFreeCore. The proof extracts the left factor of the squareFreeCore * repeatedPart primitivity invariant supplied by ZPoly.primitiveSquareFreeDecomposition_squareFreeCore_repeatedPart_primitive.

theorem Hex.squareFreeCore_squareFreeRat_of_ne_zero (f : ZPoly) (hf : f ≠ 0) : (normalizeForFactor f).squareFreeCore.SquareFreeRat

The normalized primitive square-free part is square-free over ℚ whenever the input is nonzero. Discharges the Hex.ZPoly.SquareFreeRat core precondition of exhaustiveIntegerTrialCoreFactorsWithBound_factor_irreducible (:13443) and quadraticIntegerRootFactors?_factor_irreducible_of_primitive (:14060) when both are specialised to (normalizeForFactor f).squareFreeCore. The proof forwards the recorded square-free part's non-zeroness (from squareFreeCore_ne_zero_of_ne_zero) to ZPoly.primitiveSquareFreeDecomposition_squareFreeCore, which gives the intrinsic square-free-over-ℚ invariant of the decomposition.

theorem Hex.squareFreeCore_eq_one_of_constant_of_ne_zero (f : ZPoly) (hf : f ≠ 0) (hdeg : DensePoly.natDegree (normalizeForFactor f).squareFreeCore = 0) : (normalizeForFactor f).squareFreeCore = 1

When the normalized primitive square-free part has degree zero (and f ≠ 0), the primitive square-free decomposition forces the square-free part to be exactly 1. Exposed publicly so Mathlib-side per-branch wrappers (in particular the fast-path constant arm) can rule out the singleton-part entry from the recorded factor set.