the proof notes section 4, Lemma 5: the p-adic size of the moments U_r(t^e) = (e+1)B_e + 2rB_{e+1} (v_p ≥ -1 always, p-integral for e ≤ p-3, von Staudt-Clausen), and of the pole constants H_j^{(e)} and β_j (v_p(β_j) ≥ 0 for j < p, ≥ -2 for p ∣ j, ≥ -3 otherwise, j < p²).

theorem Zeta32.Outer.VG_of_not_dvd_den {p : ℕ} {r : ℚ} (hr : ¬p ∣ r.den) : Zeta5Irrational.VG p r 0

theorem Zeta32.Outer.VG_inv_prime {p : ℕ} [hp : Fact (Nat.Prime p)] {q : ℕ} (hq : Nat.Prime q) : Zeta5Irrational.VG p (1 / ↑q) (if q = p then -1 else 0)

theorem Zeta32.Outer.bernoulli_even_VG {p : ℕ} [hp : Fact (Nat.Prime p)] (k : ℕ) : Zeta5Irrational.VG p (bernoulli (2 * k)) (if p - 1 ∣ 2 * k then -1 else 0)

von Staudt-Clausen, in VG form: B_{2k} = z - Σ_{(q-1) ∣ 2k} 1/q.

theorem Zeta32.Outer.bernoulli'_VG {p : ℕ} [hp : Fact (Nat.Prime p)] (m : ℕ) : Zeta5Irrational.VG p (bernoulli' m) (-1)

theorem Zeta32.Outer.bernoulli'_VG_small {p : ℕ} [hp : Fact (Nat.Prime p)] (hp2 : p ≠ 2) {m : ℕ} (hm : m < p - 1) : Zeta5Irrational.VG p (bernoulli' m) 0

theorem Zeta32.Outer.two_VG {p : ℕ} : Zeta5Irrational.VG p 2 0

theorem Zeta32.Outer.moment_VG {p : ℕ} [hp : Fact (Nat.Prime p)] {r : ℚ} (hr : Zeta5Irrational.VG p r 0) (e : ℕ) : Zeta5Irrational.VG p (moment r e) (-1)

theorem Zeta32.Outer.moment_VG_small {p : ℕ} [hp : Fact (Nat.Prime p)] (hp2 : p ≠ 2) {r : ℚ} (hr : Zeta5Irrational.VG p r 0) {e : ℕ} (he : e + 3 ≤ p) : Zeta5Irrational.VG p (moment r e) 0

Harmonic sums and the pole constants

theorem Zeta32.Outer.inv_pow_VG {p : ℕ} [hp : Fact (Nat.Prime p)] {a e : ℕ} (ha : 1 ≤ a) (hap : a < p ^ 2) : Zeta5Irrational.VG p (1 / ↑a ^ e) (-↑e)

theorem Zeta32.Outer.inv_pow_VG_small {p : ℕ} [hp : Fact (Nat.Prime p)] {a e : ℕ} (ha : 1 ≤ a) (hap : a < p) : Zeta5Irrational.VG p (1 / ↑a ^ e) 0

theorem Zeta32.Outer.H_VG {p : ℕ} [hp : Fact (Nat.Prime p)] {e j : ℕ} (hj : j < p ^ 2) : Zeta5Irrational.VG p (H e j) (-↑e)

theorem Zeta32.Outer.H_VG_small {p : ℕ} [hp : Fact (Nat.Prime p)] {e j : ℕ} (hj : j < p) : Zeta5Irrational.VG p (H e j) 0

def Zeta32.Outer.betaWt (p j : ℕ) : ℚ

The weight of the constant min(v_p(2j), v_p(β_j)) in the proof notes, Lemma 5.

Equations

• Zeta32.Outer.betaWt p j = if j < p then 0 else if p ∣ j then -2 else -3

theorem Zeta32.Outer.nat_VG_dvd {p : ℕ} [hp : Fact (Nat.Prime p)] (j : ℕ) (hj : 0 < j) : Zeta5Irrational.VG p (↑j) (if p ∣ j then 1 else 0)

theorem Zeta32.Outer.beta_VG {p : ℕ} [hp : Fact (Nat.Prime p)] {r : ℚ} (hr : Zeta5Irrational.VG p r 0) {j : ℕ} (hj : j < p ^ 2) : Zeta5Irrational.VG p (beta r j) (betaWt p j)

theorem Zeta32.Outer.poleValue_GV {p : ℕ} [hp : Fact (Nat.Prime p)] {r : ℚ} (hr : Zeta5Irrational.VG p r 0) {j : ℕ} (hj0 : 0 < j) (hj : j < p ^ 2) : Zeta5Irrational.GV p (Polynomial.C (2 * ↑j) * Polynomial.X + Polynomial.C (beta r j)) (betaWt p j)

GV of the linear pole value 2jX + β_j.