The class-wise bound for the polynomial part

For every integer m, v_p(P(m)) ≥ β where P is the polynomial part of κ ∏ (x - ζ) / ∏ (x - r) and β ≤ e_c - ℓ_c for every class c.

theorem Zeta5Irrational.prod_erase_split {f : ℤ → Polynomial ℚ} (S : Finset ℤ) (q : ℤ → Prop) [DecidablePred q] (r : ℤ) : ∏ s ∈ S.erase r, f s = (∏ s ∈ (Finset.filter q S).erase r, f s) * ∏ s ∈ {x ∈ S | ¬q x}.erase r, f s

theorem Zeta5Irrational.GV_lin_comp_class {p : ℕ} [hp : Fact (Nat.Prime p)] (m ζ : ℤ) (h : ↑ζ = ↑m) : GV p ((Polynomial.X - Polynomial.C ↑ζ).comp (Polynomial.C ↑m + Polynomial.C ↑p * Polynomial.X)) 1

theorem Zeta5Irrational.GV_lin_comp {p : ℕ} [hp : Fact (Nat.Prime p)] (m ζ : ℤ) : GV p ((Polynomial.X - Polynomial.C ↑ζ).comp (Polynomial.C ↑m + Polynomial.C ↑p * Polynomial.X)) 0

theorem Zeta5Irrational.GV_numOf_comp {p : ℕ} [hp : Fact (Nat.Prime p)] (κ : ℚ) (hκ : VG p κ 0) (Z : Multiset ℤ) (m : ℤ) : GV p ((numOf κ Z).comp (Polynomial.C ↑m + Polynomial.C ↑p * Polynomial.X)) ↑(cnt p Z ↑m)

theorem Zeta5Irrational.lin_comp_eq {p : ℕ} [hp : Fact (Nat.Prime p)] {m r : ℤ} (h : ↑p ∣ r - m) : (Polynomial.X - Polynomial.C ↑r).comp (Polynomial.C ↑m + Polynomial.C ↑p * Polynomial.X) = Polynomial.C ↑p * (Polynomial.X - Polynomial.C ↑((r - m) / ↑p))

(x - r)(m + p z) = p (z - ρ) with ρ = (r - m)/p, for r ≡ m.

theorem Zeta5Irrational.VG_polyPart_eval {p : ℕ} [hp : Fact (Nat.Prime p)] (κ : ℚ) (hκ : VG p κ 0) (Z : Multiset ℤ) (Pl : Finset ℤ) (hsep : Sep p Pl) (β : ℚ) (hβ : ∀ (c : ZMod p), β ≤ ↑(cnt p Z c) - ↑(plc p Pl c).card) (m : ℤ) : VG p (Polynomial.eval (↑m) (polyPart (numOf κ Z) Pl)) β

Class-wise bound for the polynomial part.

theorem Zeta5Irrational.natDegree_numOf_le (κ : ℚ) (Z : Multiset ℤ) : (numOf κ Z).natDegree ≤ Z.card

theorem Zeta5Irrational.padicValNat_24 {p : ℕ} [hp : Fact (Nat.Prime p)] (hp5 : 5 ≤ p) : padicValNat p 24 = 0

theorem Zeta5Irrational.tauX_direct {p : ℕ} [hp : Fact (Nat.Prime p)] (hp5 : 5 ≤ p) (κ : ℚ) (hκ : VG p κ 0) (Z : Multiset ℤ) (Pl : Finset ℤ) (hsep : Sep p Pl) (hH : ∀ r ∈ Pl, dd r < p ^ 2) (hdeg : Z.card - Pl.card + 1 < p ^ 2) (β : ℚ) (hβ : ∀ (c : ZMod p), β ≤ ↑(cnt p Z c) - ↑(plc p Pl c).card) : GV p (tauX (numOf κ Z) Pl) (β - 4)

The direct bound v_p^G(τ_X(g)) ≥ min_c (e_c - ℓ_c) - 4.