theorem HexBerlekampZassenhausMathlib.checkIrreducibleCert_sound (f : Hex.ZPoly) (cert : Hex.ZPolyIrreducibilityCertificate) (hprime : ∀ primeData ∈ cert.perPrime.toList, Nat.Prime primeData.p) (hprim : (HexPolyZMathlib.toPolynomial f).IsPrimitive) (hpos : 0 < (HexPolyZMathlib.toPolynomial f).natDegree) : Hex.checkIrreducibleCert f cert = true → Irreducible (HexPolyZMathlib.toPolynomial f)

The executable integer-polynomial irreducibility checker is sound after transport to Mathlib's polynomial model, under the standard certificate side-conditions: each per-prime block uses a prime modulus, the input is primitive, and the input is non-constant. Primality is needed for Rabin irreducibility lifting and (ZMod p)[X] UFD reasoning; primitivity and non-constancy rule out trivially reducible inputs whose recorded obstructions would otherwise be vacuous.

theorem HexBerlekampZassenhausMathlib.checkIrreducibleCertLinear_sound (f : Hex.ZPoly) (cert : Hex.ZPolyIrreducibilityCertificate) (hprime : ∀ primeData ∈ cert.perPrime.toList, Nat.Prime primeData.p) (hprim : (HexPolyZMathlib.toPolynomial f).IsPrimitive) (hpos : 0 < (HexPolyZMathlib.toPolynomial f).natDegree) : Hex.checkIrreducibleCertLinear f cert = true → Irreducible (HexPolyZMathlib.toPolynomial f)

Soundness of the kernel-reducible integer checker: a certificate accepted by checkIrreducibleCertLinear on literal data certifies irreducibility of the transported polynomial. The primality hypothesis feeds both the Linear→committed checker implication and the committed checker's own soundness theorem.

theorem HexBerlekampZassenhausMathlib.irreducible_of_checkIrreducibleCertLinear (f : Hex.ZPoly) (cert : Hex.ZPolyIrreducibilityCertificate) (hprime : (cert.perPrime.all fun (primeData : Hex.PrimeFactorData) => decide (Nat.Prime primeData.p)) = true) (hcontent : decide (f.content = 1) = true) (hpos : decide (0 < Hex.DensePoly.natDegree f) = true) (hcert : Hex.checkIrreducibleCertLinear f cert = true) : Irreducible (HexPolyZMathlib.toPolynomial f)

checkIrreducibleCertLinear_sound with every side condition stated as a kernel-decidable Boolean check: primality of the recorded primes, content one, and positive executable degree. This is the exact consumption shape of the multi-prime arm of the factor_poly/irreducibility extension: it applies this theorem (through zpolyIrreducible_of_checkIrreducibleCertLinear and checkMultiPrimeCert) to a reified literal certificate with an Eq.refl true proof in each hypothesis slot, so the whole obligation is discharged by kernel reduction on literal data.