def Hex.ZPoly.translateAux (s : Int) : List Int → ZPoly

Horner fold for the Taylor shift: translateAux s cs is Σᵢ cs[i]·(X + s)^i. Structural recursion on the coefficient list keeps the whole reduction closure exposed for the kernel checks in checkIrredWitness.

Equations

• Hex.ZPoly.translateAux s [] = 0
• Hex.ZPoly.translateAux s (c :: cs) = Hex.ZPoly.translateAux s cs * (Hex.ZPoly.X + Hex.DensePoly.C s) + Hex.DensePoly.C c

def Hex.ZPoly.translate (s : Int) (f : ZPoly) : ZPoly

The Taylor shift f(X) ↦ f(X + s).

Equations

• Hex.ZPoly.translate s f = Hex.ZPoly.translateAux s (Hex.DensePoly.toArray f).toList

@[simp]

theorem Hex.ZPoly.translate_zero (s : Int) : translate s 0 = 0

Translation fixes the zero polynomial.

@[simp]

theorem Hex.ZPoly.translate_C (s c : Int) : translate s (DensePoly.C c) = DensePoly.C c

Translation fixes constant polynomials.

@[simp]

theorem Hex.ZPoly.translate_one (s : Int) : translate s 1 = 1

Translation fixes the constant one.

theorem Hex.ZPoly.translate_X (s : Int) : translate s X = X + DensePoly.C s

Translating X by s yields X + s.

theorem Hex.ZPoly.translate_add (s : Int) (p q : ZPoly) : translate s (p + q) = translate s p + translate s q

translate is additive.

theorem Hex.ZPoly.translate_mul (s : Int) (a b : ZPoly) : translate s (a * b) = translate s a * translate s b

translate is multiplicative.

theorem Hex.ZPoly.translate_neg_translate (s : Int) (f : ZPoly) : translate (-s) (translate s f) = f

Shifting by s then by -s is the identity: f(X + s)(X - s) = f.

theorem Hex.ZPoly.size_translate (s : Int) (f : ZPoly) : DensePoly.size (translate s f) = DensePoly.size f

The Taylor shift preserves the dense size (hence the degree).

theorem Hex.ZPoly.isUnit_translate_iff (s : Int) (f : ZPoly) : (translate s f).IsUnit ↔ f.IsUnit

The Taylor shift preserves units (C 1 and C (-1) are fixed points in both directions).

theorem Hex.ZPoly.irreducible_of_translate_irreducible (s : Int) (f : ZPoly) (h : (translate s f).Irreducible) : f.Irreducible

Irreducibility transfers backwards through the Taylor shift: any factorization of f shifts to a factorization of translate s f, whose unit factor reflects back through the inverse shift.

theorem Hex.ZPoly.irreducible_of_eisenstein (g : ZPoly) (q : Nat) (hq : Nat.Prime q) (hprim : g.Primitive) (hsize : 1 < DensePoly.size g) (hlead : ¬↑q ∣ DensePoly.coeff g (DensePoly.size g - 1)) (hlow : ∀ (i : Nat), i < DensePoly.size g - 1 → ↑q ∣ DensePoly.coeff g i) (hsq : ¬↑q * ↑q ∣ DensePoly.coeff g 0) : g.Irreducible

Eisenstein's criterion for integer polynomials, Mathlib-free: a primitive non-constant g is irreducible when some prime q divides every coefficient below the leading one, does not divide the leading coefficient, and its square does not divide the constant term.

theorem Hex.ZPoly.irreducible_of_eisensteinCert (f : ZPoly) (q : Nat) (shift : Int) (hp : Nat.isPrimeTrial q = true) (hcontent : decide ((translate shift f).content = 1) = true) (hsize : decide (1 < DensePoly.size (translate shift f)) = true) (hlead : decide (DensePoly.coeff (translate shift f) (DensePoly.size (translate shift f) - 1) % ↑q = 0) = false) (hlow : ((List.range (DensePoly.size (translate shift f) - 1)).all fun (i : Nat) => decide (DensePoly.coeff (translate shift f) i % ↑q = 0)) = true) (hsq : decide (DensePoly.coeff (translate shift f) 0 % (↑q * ↑q) = 0) = false) : f.Irreducible

Kernel-decidable Eisenstein-after-shift irreducibility: every hypothesis is a Boolean check on the literal shifted polynomial translate shift f, whose computation is itself part of the kernel check (the translate reduction closure is exposed). Primitivity is checked on the shifted polynomial, and the resulting irreducibility transfers back through irreducible_of_translate_irreducible. Divisibility is checked through % because the free layer carries no Decidable ((q : Int) ∣ x) instance.