S4: entrywise congruence G ≡ Ref with excess 1/2, the determinant congruence det G ≡ det Ref (mod p^{Σπ+1}), and the scaled congruence p^{-Σπ} det(T)^2 · Q_{p-1} ≡ (unit) (mod p). No sorry in this file.

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

theorem Zeta32.PrimeEdge.VG_of_unit {p : ℕ} {q : ℚ} (hq : padicValRat p q = 0) : Zeta5Irrational.VG p q 0

theorem Zeta32.PrimeEdge.G_GV {p : ℕ} [hp : Fact (Nat.Prime p)] (hp7 : 7 ≤ p) {r : ℚ} (hr : Zeta5Irrational.VG p r 0) (a c : Idx p) : Zeta5Irrational.GV p (G r p a c) (rho p a + rho p c)

theorem Zeta32.PrimeEdge.Ref_GV {p : ℕ} [hp : Fact (Nat.Prime p)] (hp7 : 7 ≤ p) (w : ℕ → ℚ) (hw : ∀ b < p, w b ≠ 0 ∧ padicValRat p (w b) = 0) (a c : Idx p) : Zeta5Irrational.GV p (Ref p w a c) (rho p a + rho p c)

theorem Zeta32.PrimeEdge.G_sub_Ref_GV {p : ℕ} [hp : Fact (Nat.Prime p)] (hp7 : 7 ≤ p) {r : ℚ} (hr : Zeta5Irrational.VG p r 0) (w : ℕ → ℚ) (hsame : ∀ (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)) (a c : Idx p) : Zeta5Irrational.GV p (G r p a c - Ref p w a c) (rho p a + rho p c + 1 / 2)

S4-entry. G_{ac} - Ref_{ac} has excess ≥ 1/2 over ρ_a + ρ_c.

theorem Zeta32.PrimeEdge.rho_sum (p : ℕ) : ∑ a : Idx p, rho p a + ∑ a : Idx p, rho p a = ↑(levelSum p)

theorem Zeta32.PrimeEdge.scaled_Q_congruence {p : ℕ} [hp : Fact (Nat.Prime p)] (r : ℚ) (hp7 : 7 ≤ p) (hE : p ∉ exceptional) (hden : ¬p ∣ r.den) : ∃ (s : ℚ) (c : ℚ), s ≠ 0 ∧ c ≠ 0 ∧ padicValRat p c = 0 ∧ Zeta5Irrational.GV p (Polynomial.C s * Q r (p - 1) - Polynomial.C c) 1

S4. The scaled congruence: s · Q_{p-1} ≡ c (mod p) with c a p-adic unit.