theorem Hex.ZPoly.irreducible_of_modPCert (f : ZPoly) (p : Nat) [ZMod64.Bounds p] (m : FpPoly p) (c : ZMod64 p) (cert : Berlekamp.IrreducibilityCertificate) (hp : Nat.isPrimeTrial p = true) (hcontent : decide (f.content = 1) = true) (hadm : decide (f.leadingCoeffModP p ≠ 0) = true) (hsize : decide (1 < DensePoly.size f) = true) (hc : decide (c = 0) = false) (hfm : (DensePoly.scale c m).beqCoeffs (modP p f) = true) (hcheck : Berlekamp.checkMonicCert m cert = true) : f.Irreducible

Kernel-decidable single-prime irreducibility for f : ZPoly: f is primitive and non-constant, its reduction mod the trial-division prime p reconstructs as scale c m for a monic m with a passing Rabin certificate, and the leading coefficient survives the reduction. Fails to apply (no slot reduces to true) exactly when no single prime witnesses irreducibility; balanced inputs need the multi-prime degree-obstruction certificate from the Mathlib correspondence.

theorem Hex.ZPoly.eq_C_coeff_zero_of_size_one {f : ZPoly} (h : DensePoly.size f = 1) : f = DensePoly.C (DensePoly.coeff f 0)

A dense-size-one polynomial is the constant on its zeroth coefficient.

structure Hex.ZPoly.ModPWitness : Type

A single-prime modular irreducibility witness for a ZPoly factor, packing its own modulus and bounds instance (the PrimeFactorData idiom) so witnesses at different primes share one type.

• p : Nat

  The witnessing prime.

• bounds : ZMod64.Bounds self.p

  Bounds instance for the modulus.

• m : FpPoly self.p

  The monic image of the reduction mod p.

• c : ZMod64 self.p

  The leading unit of the reduction mod p.

• cert : Berlekamp.IrreducibilityCertificate

  Rabin certificate for m.

inductive Hex.ZPoly.IrredWitness : Type

One irreducibility witness for a ZPoly: a prime constant, a primitive linear, a single-prime modular reduction certificate, or an Eisenstein-after-shift certificate.

• primeConst : IrredWitness

  The polynomial is a constant with prime absolute value.

• linear : IrredWitness

  The polynomial is linear (dense size two) and primitive.

• modP (w : ModPWitness) : IrredWitness

  Single-prime method: the reduction mod w.p is irreducible.

• eisenstein (q : Nat) (shift : Int) : IrredWitness

  Eisenstein method: ZPoly.translate shift f satisfies Eisenstein's criterion at the prime q.

def Hex.ZPoly.checkIrredWitness (f : ZPoly) : IrredWitness → Bool

Kernel-decidable check that w witnesses irreducibility of f.

Equations

• One or more equations did not get rendered due to their size.
• f.checkIrredWitness Hex.ZPoly.IrredWitness.primeConst = (decide (Hex.DensePoly.size f = 1) && Hex.ZPoly.isNatPrime (Hex.DensePoly.coeff f 0).natAbs)
• f.checkIrredWitness Hex.ZPoly.IrredWitness.linear = (decide (Hex.DensePoly.size f = 2) && decide (f.content = 1))

theorem Hex.ZPoly.irreducible_of_checkIrredWitness (f : ZPoly) (w : IrredWitness) (hcheck : f.checkIrredWitness w = true) : f.Irreducible

A passing checkIrredWitness forces irreducibility.

def Hex.ZPoly.checkIrredCover (factors : List ZPoly) (certified : List (ZPoly × IrredWitness)) : Bool

Bulk kernel-decidable irreducibility for a ZPoly factor list with repetition: certified carries one (factor, witness) entry per distinct factor, matched by beqCoeffs, so each witness is checked once regardless of multiplicity.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.ZPoly.irreducible_of_checkIrredCover (factors : List ZPoly) (certified : List (ZPoly × IrredWitness)) (hcheck : checkIrredCover factors certified = true) (q : ZPoly) : q ∈ factors → q.Irreducible

A passing checkIrredCover forces irreducibility of every listed factor. The single Boolean hypothesis is the factors_irred slot of a reified ZPoly.Factored value.