S2b-1: the proof notes, Lemma 1 / Corollary 2 (the p-adic distribution formula for U_r), in the truncated rational form used by §6.

Exact statement behind it (in ℚ_p): U_r(f) = p^{-2} Σ_{b<p} V_Y(g_b) with Y = p³X + C_p, C_p ∈ p³ℤ_p. Taking the X-free part, the difference between (Lfun r n A).coeff 0 and p^{-2} Σ_b discLocal r n p b A consists of

• the -2 C_p near-pole terms: valuation ≥ β + 1 (v(C_p) ≥ 3, near residues have Gauss valuation ≥ e(-b) + [b = 0], near-pole denominators ∏ (m' - m) are units since m, m' < p);
• the far-pole tails of degree ≥ truncOrder n = 10n + 2: the coefficient of u^e in dissectNum / farProd has valuation ≥ e(-b) + [b=0] + e - (10n - 1) and V loses at most 1 (von Staudt), so each tail term has valuation ≥ β. Hence the error has valuation ≥ β - 1, one more than the size β - 2 of the entry (Lfun_GV).

proof (files Dist/*). No ℚ_p constants are needed. Write t A = P · D_{5n} + ∑_j c_j D_{5n}/(t+j) (XA_pf); both sides are linear in the numerator.

• On P · D_{5n} the formula is exact (Err_poly: multiplication theorem Psi_eq).
• On D_{5n}/(t+j): the near disc b = j mod p gives p^{-3} V^loc(1/(u+⌊j/p⌋)), which cancels the p-divisible part of H^{(3)}_j, H^{(2)}_j (VG_near_cancel); every far disc gives a p-integral value (VG_far). So the error on one pole has valuation ≥ -2 (VG_Err_Ej).
• v_p(c_j) ≥ β + 1 (VG_res, and p ∣ j when j is in the class 0).

theorem Zeta32.PrimeEdge.nearS_lt {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} (hn : 5 * n < p ^ 2) (b m : ℕ) : m ∈ nearSet n p b → m < p

theorem Zeta32.PrimeEdge.VG_inv_sub {p : ℕ} [hp : Fact (Nat.Prime p)] {j b : ℕ} (hb : b < p) (hjb : j % p ≠ b) : Zeta5Irrational.VG p (↑j - ↑b)⁻¹ 0

theorem Zeta32.PrimeEdge.VG_Err_Ej {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} (hn : 5 * n < p ^ 2) {r : ℚ} (hr : Zeta5Irrational.VG p r 0) {j : ℕ} (hj : j ∈ Finset.Icc 1 (5 * n)) : Zeta5Irrational.VG p (Err r n p (Ej (Finset.Icc 1 (5 * n)) j)) (-2)

The error on one simple pole has valuation ≥ -2.

theorem Zeta32.PrimeEdge.distribution_trunc {p : ℕ} [Fact (Nat.Prime p)] {n : ℕ} (hn1 : 1 ≤ n) (hn : 5 * n < p ^ 2) {r : ℚ} (hr : Zeta5Irrational.VG p r 0) {A : Polynomial ℚ} {e : ZMod p → ℤ} (hA : Arith.Local.Adm p A e) (hdeg : A.natDegree + 2 ≤ 10 * n) (β : ℚ) (hβ : ∀ (γ : ZMod p), β ≤ (↑(e γ) + if γ = 0 then 1 else 0) - ↑(Arith.Local.plc p (Arith.Local.Pl5 n) γ).card) : Zeta5Irrational.VG p ((Arith.Local.Lfun r n A).coeff 0 - ↑p ^ (-2) * ∑ b ∈ Finset.range p, discLocal r n p b A) (β - 1)

S2b-1 (truncated distribution formula). Hypotheses as in Lfun_GV.