Bookkeeping for the proof notes section 8.2: the exact valuation of the normalizer S_n^{3n}/F_n (Legendre with one level, 5n < p²), the row product ∏ rowScale = p^{5n+1-p}, and the sum of the class bounds over all classes. normScale_val and the floor sums are adapted from dtq1997/li2-half-irrationality@d5d8206:Li2Unified/Modular/Base/ DecayMediumClosed.lean and MediumFloorSum.lean (layout 2n, 4n, 3 there, 3n, 5n, 4 here).

The normalizer

theorem Zeta32.Outer.padicValRat_prod_range (p : ℕ) [Fact (Nat.Prime p)] (f : ℕ → ℚ) (hf : ∀ (i : ℕ), f i ≠ 0) (N : ℕ) : padicValRat p (∏ i ∈ Finset.range N, f i) = ∑ i ∈ Finset.range N, padicValRat p (f i)

def Zeta32.Outer.normVal (p n : ℕ) : ℚ

Prime-valuation normalization term for the scaled determinant.

Equations

• Zeta32.Outer.normVal p n = 3 * ↑n * (↑(5 * n / p) - 4 * ↑(n / p)) - 2 * ∑ i ∈ Finset.range (3 * n), ↑(i / p)

theorem Zeta32.Outer.scale_val (p : ℕ) [hp : Fact (Nat.Prime p)] {n : ℕ} (hK : 5 * n < p ^ 2) : ↑(padicValRat p (scale n)) = normVal p n

theorem Zeta32.Outer.scale_VG (p : ℕ) [Fact (Nat.Prime p)] {n : ℕ} (hK : 5 * n < p ^ 2) : Zeta5Irrational.VG p (scale n) (normVal p n)

theorem Zeta32.Outer.floor_sum_small {p n : ℕ} (hp : 0 < p) (h : 3 * n < 2 * p) : ∑ i ∈ Finset.range (3 * n), ↑(i / p) = ↑(3 * n - p)

For 3n < 2p the floor sum Σ_{i<3n} ⌊i/p⌋ is (3n - p)₊.

The row product

theorem Zeta32.Outer.rowScale_prod {n p : ℕ} (h1 : 2 * n + 1 ≤ p) (h2 : p ≤ 5 * n + 1) : ∏ a : Fin (3 * n), rowScale n p ↑a = ↑p ^ (5 * n + 1 - p)

Summing the class bounds

theorem Zeta32.Outer.sum_range_ite_lt (N r : ℕ) : (∑ c ∈ Finset.range N, if c < r then 1 else 0) = ↑(min N r)

def Zeta32.Outer.gcl (n p c : ℕ) : ℚ

The per-class lower bound of Classes.lean.

Equations

• Zeta32.Outer.gcl n p c = if c + 1 = p then -4 else if c < n then -if c < 5 * n - 2 * p then 1 else 0 else -4 * if c < 5 * n - p then 1 else 0

theorem Zeta32.Outer.Scl_ge_gcl {n p c : ℕ} (h73 : 7 * n < 3 * p) (hp5 : p ≤ 5 * n) (hc : c < p) : gcl n p c ≤ Scl n p c

theorem Zeta32.Outer.sum_gcl {n p : ℕ} (h73 : 7 * n < 3 * p) (hp5 : p ≤ 5 * n) : ∑ c : Fin p, gcl n p ↑c = -4 - ↑(5 * n - 2 * p) - 4 * ↑(min (p - 1 - n) (5 * n - p - n))