theorem HexBerlekampZassenhausMathlib.factorClassicalFactors_factor_irreducible (f : Hex.ZPoly) (hf : f ≠ 0) {cf : Array Hex.ZPoly} (hcf : Hex.factorClassicalFactors f = some cf) {raw : Hex.ZPoly} (hmem : raw ∈ cf.toList) (hrec : Hex.shouldRecordPolynomialFactor (Hex.normalizeFactorSign raw) = true) : raw.Irreducible

Every recordable raw factor returned by the direct classical method is irreducible.

theorem HexBerlekampZassenhausMathlib.proposedFactorization_factor_irreducible (f : Hex.ZPoly) (hf : f ≠ 0) (result : Hex.ProposedFactorization f) {raw : Hex.ZPoly} (hmem : raw ∈ result.factors.toList) (hrec : Hex.shouldRecordPolynomialFactor (Hex.normalizeFactorSign raw) = true) : raw.Irreducible

A successful proposal is irreducible factorwise because its flattened array is exactly the output of proved classical factorization calls.

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

Hybrid raw-factor irreducibility, selecting over proposal replay, direct classical, lattice, and trial sources.