the proof notes, §3 Lemma 4 bounds for the CRT-basis entries (n = p - 1), and the slope (X-coefficient) bound of the Remark after Lemma 4.

Conventions of Arith/Local: Adm p A e bounds the Gauss valuation of A(m + p x) by e (m mod p); the poles of Lfun are -j, j ∈ [1, 5n], and the class γ : ZMod p of the pole -j corresponds to the disc d = (-γ).val = j mod p.

def Zeta32.PrimeEdge.entExp (p : ℕ) (a c : Idx p) (γ : ZMod p) : ℤ

Adm exponent of Aent a c = φ_a φ_c D_{p-1}^4 at the class γ (disc d = (-γ).val): 4 [d ≠ 0] from D_{p-1}^4 plus the basis multiplicities.

Equations

• Zeta32.PrimeEdge.entExp p a c γ = (if (-γ).val = 0 then 0 else 4) + ↑(Zeta32.PrimeEdge.kmul p a (-γ).val) + ↑(Zeta32.PrimeEdge.kmul p c (-γ).val)

def Zeta32.PrimeEdge.poleCount (p d : ℕ) : ℕ

Number of poles j ∈ [1, 5(p-1)] with j ≡ d (mod p).

Equations

• Zeta32.PrimeEdge.poleCount p d = if d = 0 then 4 else if d + 5 ≤ p then 5 else 4

theorem Zeta32.PrimeEdge.five_mul_lt_sq {p : ℕ} (hp : 5 ≤ p) : 5 * (p - 1) < p ^ 2

theorem Zeta32.PrimeEdge.Adm_Aent {p : ℕ} [Fact (Nat.Prime p)] (hp : 5 ≤ p) (a c : Idx p) : Arith.Local.Adm p (Aent p a c) (entExp p a c)

S2-Adm. Class-wise Gauss valuations of the entry numerator.

theorem Zeta32.PrimeEdge.card_residue_of_iff {p d : ℕ} (hdp : d < p) (T : Finset ℕ) (hT : ∀ (t : ℕ), 1 ≤ d + p * t ∧ d + p * t ≤ 5 * (p - 1) ↔ t ∈ T) : {j ∈ Finset.Icc 1 (5 * (p - 1)) | j % p = d}.card = T.card

S2-count (pure ℕ). #{j ∈ [1, 5(p-1)] : j ≡ d (mod p)} is 4, 5, 4 for d = 0, 1 ≤ d ≤ p-5, d ≥ p-4 (j = d + p t; cf. Nat.Ico_filter_modEq_card).

theorem Zeta32.PrimeEdge.card_residue_Icc {p : ℕ} (hp : 5 ≤ p) {d : ℕ} (hd : d < p) : {j ∈ Finset.Icc 1 (5 * (p - 1)) | j % p = d}.card = poleCount p d

theorem Zeta32.PrimeEdge.card_plc_Pl5 {p : ℕ} [Fact (Nat.Prime p)] (hp : 5 ≤ p) (γ : ZMod p) : (Arith.Local.plc p (Arith.Local.Pl5 (p - 1)) γ).card = poleCount p (-γ).val

Pole count per class (reduction adapted from card_plc_Pl5 in Zeta32/Arith/Greedy.lean).

theorem Zeta32.PrimeEdge.entExp_hβ {p : ℕ} [Fact (Nat.Prime p)] (hp : 5 ≤ p) (a c : Idx p) (β : ℚ) (hβ : ∀ d < p, β ≤ ↑(discExp p a c d)) (γ : ZMod p) : β + 2 ≤ (↑(entExp p a c γ) + if γ = 0 then 1 else 0) - ↑(Arith.Local.plc p (Arith.Local.Pl5 (p - 1)) γ).card

The Lemma 4 hypothesis of Lfun_GV in terms of discExp.

theorem Zeta32.PrimeEdge.entry_GV {p : ℕ} [Fact (Nat.Prime p)] (hp : 5 ≤ p) {r : ℚ} (hr : Zeta5Irrational.VG p r 0) (a c : Idx p) (β : ℚ) (hβ : ∀ d < p, β ≤ ↑(discExp p a c d)) : Zeta5Irrational.GV p (G r p a c) β

Lemma 4 for one entry (from Lfun_GV): v(G_{ac}) ≥ min_d discExp a c d.

theorem Zeta32.PrimeEdge.cross_VG {p : ℕ} [Fact (Nat.Prime p)] (hp : 5 ≤ p) {r : ℚ} (hr : Zeta5Irrational.VG p r 0) (a c : Idx p) (hac : a.fst ≠ c.fst) : Zeta5Irrational.GV p (G r p a c) (rho p a + rho p c + 1 / 2)

S2c. Entries between two different classes have excess ≥ 1/2 (no tie).

theorem Zeta32.PrimeEdge.slope_VG {p : ℕ} [Fact (Nat.Prime p)] (hp : 5 ≤ p) (r : ℚ) (a c : Idx p) : Zeta5Irrational.VG p ((G r p a c).coeff 1) (rho p a + rho p c + 3)

S2a. The coefficient of X has excess ≥ 3 (Remark after Lemma 4): it is Σ_j res_j · 2j, and VG_res with Adm_Aent, card_plc_Pl5 gives v(res_j · 2j) ≥ discExp a c d + 3 for the disc d ≡ j.

theorem Zeta32.PrimeEdge.Lfun_coeff_of_two_le (r : ℚ) (n : ℕ) (A : Polynomial ℚ) {k : ℕ} (hk : 2 ≤ k) : (Arith.Local.Lfun r n A).coeff k = 0

theorem Zeta32.PrimeEdge.GV_Lfun_sub_C {p : ℕ} {r : ℚ} {n : ℕ} {A : Polynomial ℚ} {q β : ℚ} (h0 : Zeta5Irrational.VG p ((Arith.Local.Lfun r n A).coeff 0 - q) β) (h1 : Zeta5Irrational.VG p ((Arith.Local.Lfun r n A).coeff 1) β) : Zeta5Irrational.GV p (Arith.Local.Lfun r n A - Polynomial.C q) β