p-adic estimates for S2b-1.

• dist_VG_bernoulli_B : v_p(B'_k) ≥ -1 (von Staudt–Clausen);
• dist_VG_locMoment : v_p(V(u^e)) ≥ -1, and V(1) = 2 s;
• GV_divByMonic_mprod : division by ∏ (u + m) keeps the Gauss valuation;
• VG_locValue : Lemma 3 type bound v_p(locValue s R M) ≥ c - 1 if GV R c, M ⊆ [0, p);
• VG_locPoly_tate : v_p(locPoly s F) ≥ 0 if v_p(F_e) ≥ e and v_p(s) ≥ 1;
• H_split : H_e(j) = p^{-e} H_e(⌊j/p⌋) + ∑_{a ≤ j, p ∤ a} a^{-e}.

theorem Zeta32.PrimeEdge.VG_inv_prime {p : ℕ} [hp : Fact (Nat.Prime p)] {q : ℕ} (hq : Nat.Prime q) : Zeta5Irrational.VG p (↑q)⁻¹ (-1)

theorem Zeta32.PrimeEdge.dist_VG_bernoulli_B {p : ℕ} [hp : Fact (Nat.Prime p)] (k : ℕ) : Zeta5Irrational.VG p (bernoulli' k) (-1)

von Staudt–Clausen: v_p(B'_k) ≥ -1.

theorem Zeta32.PrimeEdge.dist_VG_locMoment {p : ℕ} [hp : Fact (Nat.Prime p)] {s : ℚ} (hs : Zeta5Irrational.VG p s 0) (e : ℕ) : Zeta5Irrational.VG p (locMoment s e) (-1)

theorem Zeta32.PrimeEdge.locMoment_zero (s : ℚ) : locMoment s 0 = 2 * s

theorem Zeta32.PrimeEdge.GV_divByMonic_X_add_C {p : ℕ} [hp : Fact (Nat.Prime p)] {R : Polynomial ℚ} {c : ℚ} (hR : Zeta5Irrational.GV p R c) (a : ℕ) : Zeta5Irrational.GV p (R /ₘ (Polynomial.X + Polynomial.C ↑a)) c

theorem Zeta32.PrimeEdge.divByMonic_X_add_C_mul (R : Polynomial ℚ) (a : ℚ) {g : Polynomial ℚ} (hg : g.Monic) : R /ₘ ((Polynomial.X + Polynomial.C a) * g) = R /ₘ (Polynomial.X + Polynomial.C a) /ₘ g

theorem Zeta32.PrimeEdge.GV_divByMonic_mprod {p : ℕ} [hp : Fact (Nat.Prime p)] {R : Polynomial ℚ} {c : ℚ} (hR : Zeta5Irrational.GV p R c) (M : Finset ℕ) : Zeta5Irrational.GV p (R /ₘ mprod M) c

theorem Zeta32.PrimeEdge.VG_eval_GV {p : ℕ} [hp : Fact (Nat.Prime p)] {R : Polynomial ℚ} {c z : ℚ} (hR : Zeta5Irrational.GV p R c) (hz : Zeta5Irrational.VG p z 0) : Zeta5Irrational.VG p (Polynomial.eval z R) c

theorem Zeta32.PrimeEdge.VG_locPoly {p : ℕ} [hp : Fact (Nat.Prime p)] {s : ℚ} (hs : Zeta5Irrational.VG p s 0) {Q : Polynomial ℚ} {c : ℚ} (hQ : Zeta5Irrational.GV p Q c) : Zeta5Irrational.VG p (locPoly s Q) (c - 1)

theorem Zeta32.PrimeEdge.int_not_dvd_of_lt {p : ℕ} [hp : Fact (Nat.Prime p)] {m m' : ℕ} (hm : m < p) (hm' : m' < p) (hne : m' ≠ m) : ¬↑p ∣ ↑m' - ↑m

theorem Zeta32.PrimeEdge.VG_denom_inv {p : ℕ} [hp : Fact (Nat.Prime p)] (M : Finset ℕ) (hM : ∀ m ∈ M, m < p) {m : ℕ} (hm : m ∈ M) : Zeta5Irrational.VG p (∏ m' ∈ M.erase m, (↑m' - ↑m))⁻¹ 0

Near-pole denominators are units.

theorem Zeta32.PrimeEdge.VG_inv_pow_of_not_dvd {p : ℕ} [hp : Fact (Nat.Prime p)] {a : ℕ} (ha : ¬p ∣ a) (e : ℕ) : Zeta5Irrational.VG p (1 / ↑a ^ e) 0

theorem Zeta32.PrimeEdge.VG_H {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : m < p) (e : ℕ) : Zeta5Irrational.VG p (H e m) 0

theorem Zeta32.PrimeEdge.dist_VG_locPole {p : ℕ} [hp : Fact (Nat.Prime p)] {s : ℚ} (hs : Zeta5Irrational.VG p s 0) {m : ℕ} (hm : m < p) : Zeta5Irrational.VG p (locPole s m) 0

theorem Zeta32.PrimeEdge.VG_locValue {p : ℕ} [hp : Fact (Nat.Prime p)] {s : ℚ} (hs : Zeta5Irrational.VG p s 0) (M : Finset ℕ) (hM : ∀ m ∈ M, m < p) {R : Polynomial ℚ} {c : ℚ} (hR : Zeta5Irrational.GV p R c) : Zeta5Irrational.VG p (locValue s R M) (c - 1)

Local integrality (Lemma 3 type): v_p(locValue s R M) ≥ c - 1.

theorem Zeta32.PrimeEdge.VG_locPoly_tate {p : ℕ} [hp : Fact (Nat.Prime p)] {s : ℚ} (hs : Zeta5Irrational.VG p s 1) {F : Polynomial ℚ} (hF : ∀ (e : ℕ), Zeta5Irrational.VG p (F.coeff e) ↑e) : Zeta5Irrational.VG p (locPoly s F) 0

v_p(locPoly s F) ≥ 0 if v_p(F_e) ≥ e and v_p(s) ≥ 1.

theorem Zeta32.PrimeEdge.H_split {p : ℕ} [hp : Fact (Nat.Prime p)] (e j : ℕ) : H e j = (↑p ^ e)⁻¹ * H e (j / p) + ∑ a ∈ Finset.Icc 1 j with ¬p ∣ a, 1 / ↑a ^ e

H_e(j) = p^{-e} H_e(⌊j/p⌋) + ∑_{a ≤ j, p ∤ a} a^{-e}.

theorem Zeta32.PrimeEdge.VG_sum_not_dvd {p : ℕ} [hp : Fact (Nat.Prime p)] (e j : ℕ) : Zeta5Irrational.VG p (∑ a ∈ Finset.Icc 1 j with ¬p ∣ a, 1 / ↑a ^ e) 0

theorem Zeta32.PrimeEdge.VG_near_cancel {p : ℕ} [hp : Fact (Nat.Prime p)] {r : ℚ} (hr : Zeta5Irrational.VG p r 0) (j : ℕ) : Zeta5Irrational.VG p (locPole r j - (↑p ^ 3)⁻¹ * locPole (r * ↑p) (j / p)) 0

Near-pole cancellation: V(1/(t+j)) - p^{-3} V^loc(1/(u + ⌊j/p⌋)) is integral.