the proof notes, §8.1 (ii): the column values colVal n p b through the residues r₀ = n % p, s₀ = 5n % p, and the closed forms of Σ_b c_b and Σ_b c_b² (the column multiset β+1 once, β+3 μ times, β−1 (s₀−μ) times, β+4 (r₀−μ) times, β otherwise).

theorem Zeta32.Arith.Relaxed.card_filter_mod_Icc (p b : ℕ) (hp : 0 < p) (hb : b < p) (n : ℕ) : {i ∈ Finset.Icc 1 n | i % p = b}.card = n / p + if 1 ≤ b ∧ b ≤ n % p then 1 else 0

#{1 ≤ i ≤ n : i ≡ b mod p} = ⌊n/p⌋ + [1 ≤ b ≤ n mod p] for b < p.

noncomputable def Zeta32.Arith.Relaxed.ind (c r : ℕ) : ℝ

Real indicator [c < r].

Equations

• Zeta32.Arith.Relaxed.ind c r = if c < r then 1 else 0

theorem Zeta32.Arith.Relaxed.sum_ind {m r : ℕ} (hr : r ≤ m) : ∑ c ∈ Finset.range m, ind c r = ↑r

theorem Zeta32.Arith.Relaxed.colVal_succ (n p c A L r₀ s₀ : ℕ) (hp : 0 < p) (hc : c + 1 < p) (hA : n / p = A) (hL : 5 * n / p = L) (hr : n % p = r₀) (hs : 5 * n % p = s₀) : ↑(colVal n p (c + 1)) = 4 * ↑A - ↑L - 2 + 4 * ind c r₀ - ind c s₀

Column value for 1 ≤ b = c + 1 < p.

theorem Zeta32.Arith.Relaxed.colVal_zero (n p A L : ℕ) (hp : 0 < p) (hA : n / p = A) (hL : 5 * n / p = L) : ↑(colVal n p 0) = 4 * ↑A - ↑L - 2 + 1

Column value for b = 0.

theorem Zeta32.Arith.Relaxed.ind_mul_ind (c r s : ℕ) : ind c r * ind c s = ind c (min r s)

theorem Zeta32.Arith.Relaxed.ind_sq (c r : ℕ) : ind c r ^ 2 = ind c r

theorem Zeta32.Arith.Relaxed.sum_colVal (n p A L r₀ s₀ : ℕ) (hp : 0 < p) (hA : n / p = A) (hL : 5 * n / p = L) (hr : n % p = r₀) (hs : 5 * n % p = s₀) : ∑ b ∈ Finset.range p, ↑(colVal n p b) = ↑p * (4 * ↑A - ↑L - 2) + 4 * ↑r₀ - ↑s₀ + 1

Σ_b c_b = pβ + 4r₀ − s₀ + 1, β = 4A − L − 2.

theorem Zeta32.Arith.Relaxed.sum_colVal_sq (n p A L r₀ s₀ : ℕ) (hp : 0 < p) (hA : n / p = A) (hL : 5 * n / p = L) (hr : n % p = r₀) (hs : 5 * n % p = s₀) : ∑ b ∈ Finset.range p, ↑(colVal n p b) ^ 2 = ↑p * (4 * ↑A - ↑L - 2) ^ 2 + 2 * (4 * ↑A - ↑L - 2) * (4 * ↑r₀ - ↑s₀ + 1) + 1 + 16 * ↑r₀ + ↑s₀ - 8 * ↑(min r₀ s₀)

Σ_b c_b² = pβ² + 2β(4r₀ − s₀ + 1) + 1 + 16r₀ + s₀ − 8μ, μ = min(r₀, s₀).