theorem HexBerlekampZassenhausMathlib.prod_map_signedSums {K : Type u_1} [CommRing K] {M : Type u_2} [CommMonoid M] {n : ℕ} (r : Fin n → K) (g : K → M) : (List.map g (signedSums (List.ofFn r))).prod = ∏ ε : Fin n → Bool, g (∑ i : Fin n, if ε i = true then r i else -r i)

The fold-built signed sums enumerate the 2ⁿ sign patterns.

Stated for an arbitrary g into an arbitrary commutative monoid, because the induction step replaces g by fun s => g (s + x) * g (s - x): the last radicand is consumed by the function, not by the list.

theorem HexBerlekampZassenhausMathlib.signPatternPoly_ofFn {K : Type u_1} [CommRing K] (c : ℤ) {n : ℕ} (r : Fin n → K) : signPatternPoly (↑c) (List.ofFn r) = Hex.SquareClass.signPoly c r

The two sign-pattern products are the same polynomial: the List.prod the iterated norm computes and the Finset.prod the tower theorem is about.

theorem HexBerlekampZassenhausMathlib.irreducible_of_check {cert : Hex.QuadraticNormCertificate} {f : Hex.ZPoly} (h : cert.check f = true) : Irreducible (HexPolyZMathlib.toPolynomial f)

The certificate is sound. A successful Hex.QuadraticNormCertificate.check makes its input irreducible in Polynomial ℤ.

No hypothesis is needed on f: the check pins f to an associate of the iterated norm, and the iterated norm is monic whatever f was.

theorem HexBerlekampZassenhausMathlib.irreducible_of_quadraticNormCertified {core : Hex.ZPoly} {width : ℕ} (h : Hex.quadraticNormCertified core width = true) : Irreducible (HexPolyZMathlib.toPolynomial core)

The production gate is sound. Whenever the budget-gated certificate reports true, its input is irreducible.