S2b-2 / S2b-3: the proof notes, §6 "Local shapes" and "Scaling", for the entries of one class block, on its own disc and on the other discs (n = p - 1).

Local shape of seriesPart / nearProd on the disc b for a = ⟨b, i⟩, c = ⟨b, k⟩ (κ(u) = (unit) (1 + O(p u)), κ(0) ≡ w_b):

• low (1 ≤ b ≤ p-5, nearSet = {0,…,4}): p^{4+i+k} u^{i+k} r_L(u) κ(u);
• high (p-4 ≤ b, nearSet = {0,…,3}): p^{4+i+k} u^{i+k} r_H(u) κ(u);
• zero (b = 0, nearSet = {1,…,4}): p^{1+i+k} u^{i+k} r_0(u) κ(u). With the p^{-|near|} of discLocal and the p^{-2} of Corollary 2 the power is p^{c_b+i+k}. Modulo one more power of p the local functional is V⁰ (the 2rp moments are ≡ 0, a moment of valuation -1 needs degree ≥ 2p-1, and each extra power of p in κ raises the degree by at most one). Expected unit weight (hint only, not checked; not needed in the statement): w_b = (-b)·∏_{b'≠b}(b'-b)^{2m_{b'}}·∏_{1≤i'≤p-1, i'≠b}(i'-b)^4 / ∏_{j∈[1,5(p-1)], j≢b}(j-b) for b ≠ 0, and the same without the factor (-b) for b = 0.

Proof (files in Disc/): Factor writes dissectNum on the disc d as p^E u^E R(u) with R scaled (u^e-coefficient of valuation ≥ e) and R(0) a unit, so the coefficient of u^e in seriesPart vanishes for e < E and has valuation ≥ e (Core). Core.VG_locValue_scaled is Lemma 3 for such numerators (LocValue, Bernoulli: von Staudt). Other disc: E - |near| - 2 ≥ 2. Own disc: w_b = K(0) for K = R_b / farProd; subtracting p^E K(0) u^E leaves a numerator vanishing to order E + 1, and V_{rp}(u^E) ≡ V⁰(u^E) mod p (degree E ≤ |near| + p - 2).

theorem Zeta32.PrimeEdge.card_1234 : {1, 2, 3, 4}.card = 4

theorem Zeta32.PrimeEdge.card_01234 : {0, 1, 2, 3, 4}.card = 5

theorem Zeta32.PrimeEdge.card_0123 : {0, 1, 2, 3}.card = 4

theorem Zeta32.PrimeEdge.other_data {p : ℕ} [Fact (Nat.Prime p)] (hp : 5 ≤ p) {d : ℕ} (hd : d < p) (a c : Idx p) (hac : a.fst = c.fst) (hdb : d ≠ ↑a.fst) : ∃ (E : ℕ) (R : Polynomial ℚ), dissectNum p d (Aent p a c) = Polynomial.C (↑p ^ E) * Polynomial.X ^ E * R ∧ Scaled p R ∧ IsUnitV p (R.coeff 0) ∧ E + 2 ≤ (nearSet (p - 1) p d).card + 2 * p ∧ (nearSet (p - 1) p d).card + 4 ≤ E

Exponent bookkeeping on another disc d: E = 2 m_d + (1 or 4), |near| ∈ {4, 5}.

theorem Zeta32.PrimeEdge.same_data {p : ℕ} (hp : 5 ≤ p) {b i k : ℕ} (hb : b < p) (hi : i < mult p b) (hk : k < mult p b) : blockMoment p b (i + k) = locValue 0 (Polynomial.X ^ (ownExp b + i + k)) (nearSet (p - 1) p b) ∧ colBase p b + ↑i + ↑k = ↑(ownExp b + i + k) - 2 - ↑(nearSet (p - 1) p b).card ∧ ownExp b + i + k + 1 + 2 ≤ (nearSet (p - 1) p b).card + 2 * p ∧ ownExp b + i + k + 2 ≤ (nearSet (p - 1) p b).card + p ∧ ownExp b + i + k < truncOrder (p - 1)

Exponent bookkeeping on the own disc b, and blockMoment as V⁰(u^E / nearProd).

theorem Zeta32.PrimeEdge.same_core {p : ℕ} [Fact (Nat.Prime p)] (hp : 5 ≤ p) {s : ℚ} (hs : Zeta5Irrational.VG p s 1) {N : Finset ℕ} (hN : N ⊆ Finset.range 5) {P : Polynomial ℚ} {E : ℕ} {K0 : ℚ} (hK0 : Zeta5Irrational.VG p K0 0) (hPc : ∀ (e : ℕ), Zeta5Irrational.VG p (P.coeff e) ↑e) (hPz : ∀ e < E, P.coeff e = 0) (hPE : P.coeff E = ↑p ^ E * K0) (hE3 : E + 1 + 2 ≤ N.card + 2 * p) (hE2 : E + 2 ≤ N.card + p) {c : ℤ} (hc : c = ↑E - 2 - ↑N.card) {B : ℚ} (hB : B = locValue 0 (Polynomial.X ^ E) N) : Zeta5Irrational.VG p (↑p ^ (-2) * (↑p ^ (-↑N.card) * locValue s P N) - ↑p ^ c * K0 * B) (↑c + 1)

The own-disc estimate, abstractly: P has u^e-coefficients of valuation ≥ e, vanishing below E, with u^E-coefficient p^E K₀.

theorem Zeta32.PrimeEdge.rho_le_half {p : ℕ} (a : Idx p) : rho p a ≤ 1 / 2

theorem Zeta32.PrimeEdge.disc_same_class {p : ℕ} [Fact (Nat.Prime p)] (hp7 : 7 ≤ p) {r : ℚ} (hr : Zeta5Irrational.VG p r 0) : ∃ (w : ℕ → ℚ), (∀ b < p, w b ≠ 0 ∧ padicValRat p (w b) = 0) ∧ ∀ (a c : Idx p), a.fst = c.fst → Zeta5Irrational.VG p (↑p ^ (-2) * discLocal r (p - 1) p (↑a.fst) (Aent p a c) - ↑p ^ (colBase p ↑a.fst + ↑↑a.snd + ↑↑c.snd) * w ↑a.fst * blockMoment p (↑a.fst) (↑a.snd + ↑c.snd)) (rho p a + rho p c + 1)

S2b-2 (own disc). For two vectors of the same class b, the disc-b local term is p^{c_b+i+k} · w_b · V⁰(u^{i+k} r_type) modulo p^{c_b+i+k+1}, with p-unit weights w_b depending only on the class.

theorem Zeta32.PrimeEdge.disc_other_class {p : ℕ} [Fact (Nat.Prime p)] (hp7 : 7 ≤ p) {r : ℚ} (hr : Zeta5Irrational.VG p r 0) (a c : Idx p) (hac : a.fst = c.fst) (d : ℕ) (hd : d < p) (hdb : d ≠ ↑a.fst) : Zeta5Irrational.VG p (↑p ^ (-2) * discLocal r (p - 1) p d (Aent p a c)) (rho p a + rho p c + 1)

S2b-3 (other discs). For two vectors of the same class b, every other disc d ≠ b contributes with excess ≥ 1: by Lemma 3 (local integrality; the degree condition holds since at most 10 near zeros occur and 10 ≤ |near| + 2p - 2) the term has valuation ≥ c_d + 2 m_d ≥ 2 ≥ ρ_a + ρ_c + 1.