theorem HexBerlekampZassenhausMathlib.TrialFactorization.factors_irreducible_of_bound (f : Hex.ZPoly) (hf_ne : f ≠ 0) (B : ℕ) (hbound : ∀ (g : Hex.ZPoly), g ∣ (Hex.normalizeForFactor f).squareFreeCore → ∀ (i : ℕ), (Hex.DensePoly.coeff g i).natAbs ≤ B) (factor : Hex.ZPoly) : factor ∈ (Hex.exhaustiveIntegerTrialCoreFactorsWithBound (Hex.normalizeForFactor f).squareFreeCore B).toList → factor.Irreducible

Mathlib-side abstract-bound wrapper for the slow-trial exhaustive arm.

Specialises the Mathlib-free Hex.exhaustiveIntegerTrialCoreFactorsWithBound_factor_irreducible (HexBerlekampZassenhaus) to the normalized square-free square-free part of an f ≠ 0 input, discharging the four input-shape hypotheses (ne_zero, Primitive, 0 < leadingCoeff, SquareFreeRat) from hf_ne via the existing helpers:

• Hex.squareFreeCore_leadingCoeff_pos_of_ne_zero for 0 < leadingCoeff (and zpoly_ne_zero_of_pos_lc for ne_zero);

• normalizeForFactor_squareFreeCore_primitive_of_ne_zero (Mathlib-side) for Primitive;

• Hex.ZPoly.primitiveSquareFreeDecomposition_squareFreeCore for SquareFreeRat.

The divisor coefficient bound hbound stays explicit so the public-bound specialisation below (B := Hex.ZPoly.defaultFactorCoeffBound f, required by the slow-trial arm of the h_raw selection in factor_entry_zpolyIrreducible_of_chosen_raw_zpolyIrreducible) can discharge it through the g ∣ (Hex.normalizeForFactor f).squareFreeCore → g ∣ f divisibility chain via primitiveSquareFreeDecomposition_reassembly_signed and the primitive-part divisibility relation.

theorem HexBerlekampZassenhausMathlib.TrialFactorization.factors_irreducible_at_input_bound (f : Hex.ZPoly) (hf_ne : f ≠ 0) (factor : Hex.ZPoly) : factor ∈ (Hex.exhaustiveIntegerTrialCoreFactorsWithBound (Hex.normalizeForFactor f).squareFreeCore f.defaultFactorCoeffBound).toList → factor.Irreducible

Input-polynomial bound specialization of factors_irreducible_of_bound at the outer bound B := Hex.ZPoly.defaultFactorCoeffBound f consumed by the slow-trial arm of the h_raw selection.

The divisor coefficient bound is discharged by lifting defaultFactorCoeffBound_valid f along Hex.squareFreeCore_dvd_self: any divisor of the primitive square-free part also divides f, so its coefficients are bounded by Hex.ZPoly.defaultFactorCoeffBound f.

theorem HexBerlekampZassenhausMathlib.TrialFactorization.reassembly_complete (f : Hex.ZPoly) (hf : f ≠ 0) : Hex.reassemblyExpansionComplete (Hex.normalizeForFactor f) (Hex.exhaustiveIntegerTrialCoreFactorsWithBound (Hex.normalizeForFactor f).squareFreeCore f.defaultFactorCoeffBound)

Slow-trial exhaustive-arm reassembly discharger (Mathlib-side).

When the slow trial path takes the exhaustive branch, the reassembly of the integer-trial factors of the square-free part of (normalizeForFactor f).squareFreeCore at the public bound B := Hex.ZPoly.defaultFactorCoeffBound f is expansion-complete. The integer-trial analog of reassemblyExpansionComplete_quadraticIntegerRootFactors_of_ne_zero: it composes the public-bound primitive-square-free-part irreducibility wrapper, the polyProduct / normalizeFactorSign / degree-positivity companions, and the non-monic expansion-complete surface reassemblyExpansionComplete_of_irreducible_squarefree_cover_of_pos_lc. Per-factor positive leading coefficient follows from the sign-normalisation identity and irreducibility; the fuel bound from the per-factor factorPower size lower bound and size_le_of_dvd_nonzero.

theorem HexBerlekampZassenhausMathlib.factorTrialFactorsWithBound_factor_irreducible (f : Hex.ZPoly) (hf : f ≠ 0) {raw : Hex.ZPoly} (hmem : raw ∈ (Hex.factorTrialFactorsWithBound f f.defaultFactorCoeffBound).toList) (hrec : Hex.shouldRecordPolynomialFactor (Hex.normalizeFactorSign raw) = true) : raw.Irreducible

Trial-branch raw-factor irreducibility (hybrid guard form).

Trial-branch raw-factor irreducibility for the cost-based hybrid, where the trial arm fires as the totality backstop. Because the deg-0 (constant-part) short-circuit is reachable, the raw output can contain the unit 1, so the statement carries the shouldRecordPolynomialFactor guard that excludes it. The two positive-degree arms reuse the quadratic and exhaustive integer-trial completeness/irreducibility content.