theorem Hex.exhaustiveIntegerTrialCoreFactorsWithBound_factor_irreducible (core : ZPoly) (B : Nat) (hcore_ne : core ≠ 0) (hcore_prim : core.Primitive) (hcore_pos : 0 < DensePoly.leadingCoeff core) (hcore_sq : core.SquareFreeRat) (hbound : ∀ (g : ZPoly), g ∣ core → ∀ (i : Nat), (DensePoly.coeff g i).natAbs ≤ B) (factor : ZPoly) : factor ∈ (exhaustiveIntegerTrialCoreFactorsWithBound core B).toList → factor.Irreducible

Every factor emitted by the standalone integer trial-division algorithm is irreducible when core is a primitive, square-free polynomial with positive leading coefficient and the bound B covers the coefficients of every divisor of core.

Three emitted-factor families are handled uniformly:

• integer-root split factors (split.1), via splitIntegerRootFactorsAux_factor_irreducible;

• peeled bounded-coefficient candidates (peel.1), via trialDivisionPeel_factor_irreducible;

• the optional final residual (peel.2, when not 1), via trialDivisionPeel_residual_irreducible.

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

Every factor emitted by quadraticIntegerRootFactors? core is a fixed point of normalizeFactorSign. For linear factors linearFactorForRoot r, the leading coefficient is 1; for the optional residual, positivity of its leading coefficient is forced by 0 < DensePoly.leadingCoeff core combined with the splitter invariant splitIntegerRootFactorsAux_polyProduct_leadingCoeff_pos. Used by the Mathlib-side discharger reassemblyExpansionComplete_quadraticIntegerRootFactors_of_ne_zero to discharge the hnorm precondition of normalizeForFactor_repeatedPart_isFactorPower_polyProduct_of_irreducible_factors_cover.

theorem Hex.quadraticIntegerRootFactors?_shouldRecord {core : ZPoly} {factors : Array ZPoly} (hcore_pos : 0 < DensePoly.leadingCoeff core) (hquad : quadraticIntegerRootFactors? core = some factors) (factor : ZPoly) : factor ∈ factors.toList → shouldRecordPolynomialFactor factor = true

Every factor returned by quadratic root extraction satisfies the factor-recording test.

theorem Hex.quadraticIntegerRootFactors?_factor_irreducible_of_ne_residual {core : ZPoly} {factors : Array ZPoly} {factor : ZPoly} (hquad : quadraticIntegerRootFactors? core = some factors) (hmem : factor ∈ factors.toList) (hnot_residual : factor ≠ (splitIntegerRootFactorsAux core (integerRootCandidates core) (integerRootCandidates core).length).snd) : factor.Irreducible

In the quadratic integer-root branch, every emitted factor other than the optional final residual comes from the integer-root splitter and is therefore irreducible. When the split is complete (residual = 1), this covers every recorded quadratic-branch factor.

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

Every factor emitted by the quadratic integer-root branch is irreducible when the square-free part is primitive with positive leading coefficient. Non-residual factors come from the integer-root splitter (linear, hence irreducible); the optional final residual is also irreducible because primitivity rules out degree-0 residuals (non-unit constants would divide every coefficient of the primitive polynomial) and the function's degree filter restricts residuals to size two, where the irreducible_of_size_two_primitive companion of _monic applies via the constant-factor argument on core.

This is the public wrapper used by Mathlib-side callers: its signature avoids referencing the file-private splitIntegerRootFactorsAux and integerRootCandidates (the residual is identified internally via case analysis).

theorem Hex.quadraticIntegerRootFactors?_product {core : ZPoly} {factors : Array ZPoly} (hquad : quadraticIntegerRootFactors? core = some factors) : factors.polyProduct = core

The factors returned by quadratic root extraction multiply to the input quadratic.

theorem Hex.polyProduct_quadraticIntegerRootFactors?_some {core : ZPoly} {coreFactors : Array ZPoly} (hquad : quadraticIntegerRootFactors? core = some coreFactors) : coreFactors.polyProduct = core

Whenever quadraticIntegerRootFactors? core returns some coreFactors, the executable Array.polyProduct of the recorded factors reconstructs core exactly. Public wrapper of the private quadraticIntegerRootFactors?_product, used by the Mathlib-side discharger reassemblyExpansionComplete_quadraticIntegerRootFactors_of_ne_zero (HexBerlekampZassenhausMathlib/IntReductionMod.lean) when feeding the factorPower repeated-part decomposition and the no-tail divisibility lemma into Hex.reassemblyExpansionComplete. The corresponding constant and small-mod singleton branch theorems are Hex.reassemblyExpansionComplete_constant_of_ne_zero and Hex.reassemblyExpansionComplete_singleton_of_irreducible.

theorem Hex.quadraticIntegerRootFactors?_factor_size_eq_two {core : ZPoly} {coreFactors : Array ZPoly} (hcore_pos : 0 < DensePoly.leadingCoeff core) (hcore_primitive : core.Primitive) (hquad : quadraticIntegerRootFactors? core = some coreFactors) {factor : ZPoly} (hmem : factor ∈ coreFactors.toList) : DensePoly.size factor = 2

Every factor emitted by quadraticIntegerRootFactors? has dense size two. The branch is only entered when core.natDegree = 2. Linear factors emitted by the splitter are linearFactorForRoot r = X - r, which has size 2 by linearFactorForRoot_size_eq_two. The optional final residual has natDegree ≤ 1 by construction, so its size is ≤ 2; the case size = 1 (constant residual) is incompatible with primitivity of core combined with positivity of leadingCoeff core (the same argument used in quadraticIntegerRootFactors?_residual_irreducible to rule out non-unit constant residuals).

Used by the Mathlib-side discharger reassemblyExpansionComplete_quadraticIntegerRootFactors_of_ne_zero to discharge the per-factor 0 < q.natDegree and 0 < leadingCoeff q preconditions of the non-monic expansion-complete surface expandRepeatedPartFactorArray_residual_eq_one_of_factorPower_decomposition_of_pos_lc.

theorem Hex.quadraticIntegerRootFactors?_pairwise_not_associated {core : ZPoly} (hcore_lc_pos : 0 < DensePoly.leadingCoeff core) (hcore_primitive : core.Primitive) (hcore_squarefree : core.SquareFreeRat) {coreFactors : Array ZPoly} (hquad : quadraticIntegerRootFactors? core = some coreFactors) : List.Pairwise (fun (q₁ q₂ : ZPoly) => ¬q₁.Associated q₂) coreFactors.toList

The factors emitted by quadraticIntegerRootFactors? core are pairwise non-ZPoly-associated whenever core is primitive, has positive leading coefficient, and is square-free over Rat[x].

Linear-vs-linear pairs follow from splitIntegerRootFactorsAux_factors_form (the splitter records linearFactorForRoot rᵢ for distinct roots rᵢ forming a Sublist of integerRootCandidates core, which is Nodup) and linearFactorForRoot_not_associated_of_ne.

Linear-vs-residual pairs are ruled out by case analysis on the ZPoly.Associated unit factor u: the u = C (-1) branch contradicts the residual's positive leading coefficient (inherited from core's positive leading coefficient via the splitter's monic-product invariant), and the u = C 1 branch produces (linearFactorForRoot r)^2 ∣ core, refuted by linearFactor_squared_not_dvd_of_squareFreeRat.

Combines with irreducible_not_dvd_of_not_associated in reassemblyExpansionComplete_quadraticIntegerRootFactors_of_ne_zero.

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

Every factor emitted by quadraticIntegerRootFactors? has positive leading coefficient when the input polynomial has positive leading coefficient. This packages the normalization and recording invariants for Mathlib-side callers of the non-monic repeated-part expansion helper.