the proof notes section 8.2, Lemma 9: the three kinds of residue classes and their class costs.

The poles j ∈ [1, 5n] are regrouped by c = (j-1) mod p (the class of j is c+1 mod p), each class listed in decreasing j: jn c t = c + 1 + p (Ccl c - 1 - t). Along a class the node weight wv is nondecreasing in t (wv_step). For 7n < 3p and p ≤ 5n the class cost Scl c = Σ_{k < Ccl c} min(wv(jn c k) + 2k, 0) satisfies

• c + 1 = p (ρ = 0): Scl c ≥ -4;
• c + 1 ≤ n (1 ≤ ρ ≤ n): Scl c ≥ -[c < 5n - 2p];
• n < c + 1 < p (n < ρ < p): Scl c ≥ -4 [c < 5n - p].

The regrouping (Ccl, jn, regroup) is adapted from dtq1997/li2-half-irrationality@d5d8206:Li2Unified/Modular/Base/DecayMediumAssembly.lean and the finite indicator sums from .../Base/MediumClassCounts.lean.

def Zeta32.Outer.Ccl (p K c : ℕ) : ℕ

Number of indices at most K in the residue class represented by c + 1.

Equations

• Zeta32.Outer.Ccl p K c = if c + 1 ≤ K then (K - (c + 1)) / p + 1 else 0

def Zeta32.Outer.jn (p K c t : ℕ) : ℕ

Descending enumeration of the residue class represented by c + 1.

Equations

• Zeta32.Outer.jn p K c t = c + 1 + p * (Zeta32.Outer.Ccl p K c - 1 - t)

theorem Zeta32.Outer.Ccl_pos (p K : ℕ) {c t : ℕ} (ht : t < Ccl p K c) : c + 1 ≤ K

theorem Zeta32.Outer.jn_le (p K : ℕ) {c t : ℕ} (ht : t < Ccl p K c) : jn p K c t ≤ K

theorem Zeta32.Outer.regroup_aux (p K : ℕ) {j : ℕ} (hp : 0 < p) (hj1 : 1 ≤ j) (hj2 : j ≤ K) : (j - 1) % p < p ∧ (j - 1) / p < Ccl p K ((j - 1) % p) ∧ jn p K ((j - 1) % p) (Ccl p K ((j - 1) % p) - 1 - (j - 1) / p) = j

theorem Zeta32.Outer.regroup_inv (p K : ℕ) {c t : ℕ} (hp : 0 < p) (hc : c < p) : (jn p K c t - 1) % p = c ∧ (jn p K c t - 1) / p = Ccl p K c - 1 - t

theorem Zeta32.Outer.regroup (p K : ℕ) {R : Type u_1} [AddCommMonoid R] (hp : 0 < p) (F : ℕ → R) : ∑ j ∈ Finset.Icc 1 K, F j = ∑ c ∈ Finset.range p, ∑ t ∈ Finset.range (Ccl p K c), F (jn p K c t)

theorem Zeta32.Outer.Ccl_eq_succ (p K : ℕ) {c : ℕ} (hc : c + 1 ≤ K) : Ccl p K c = (K - (c + 1)) / p + 1

theorem Zeta32.Outer.jn_eq (p K : ℕ) {c t C : ℕ} (hC : Ccl p K c = C) : jn p K c t = c + 1 + p * (C - 1 - t)

Node weights along a class

theorem Zeta32.Outer.wv_step {n p j d : ℕ} (hp : 0 < p) (hnj : n < j) (hK : j + p * d ≤ 5 * n) : wv n p (j + p * d) ≤ wv n p j

theorem Zeta32.Outer.betaWt_class {p c m : ℕ} (hc : c < p) : betaWt p (c + 1 + p * m) = if m = 0 ∧ c + 1 < p then 0 else if c + 1 = p then -2 else -3

theorem Zeta32.Outer.wv_class {n p c m : ℕ} (hp : 0 < p) (hnp : n < p) (hc : c < p) (hm : c + 1 + p * m ≤ 5 * n) (hj : n < c + 1 + p * m) : wv n p (c + 1 + p * m) = (if c < n then 5 else 1) - ↑(Ccl p (5 * n) c) + betaWt p (c + 1 + p * m)

theorem Zeta32.Outer.wv_cancelled {n p j : ℕ} (hj : j ≤ n) : wv n p j = 15 * ↑n + 1

Class costs

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

The Newton-form class cost of rank_one_GV.

Equations

• Zeta32.Outer.Scl n p c = ∑ k ∈ Finset.range (Zeta32.Outer.Ccl p (5 * n) c), min (Zeta32.Outer.wv n p (Zeta32.Outer.jn p (5 * n) c k) + 2 * ↑k) 0

theorem Zeta32.Outer.wv_jn {n p c C t : ℕ} (hp : 0 < p) (hnp : n < p) (hc : c < p) (hC : Ccl p (5 * n) c = C) (ht : t < C) (hj : n < c + 1 + p * (C - 1 - t)) : wv n p (jn p (5 * n) c t) = (if c < n then 5 else 1) - ↑C + betaWt p (c + 1 + p * (C - 1 - t))

theorem Zeta32.Outer.Scl_zero {n p c : ℕ} (h73 : 7 * n < 3 * p) (hp5 : p ≤ 5 * n) (hc : c + 1 = p) : -4 ≤ Scl n p c

Class ρ = 0 (c + 1 = p): the L ≤ 2 nodes kp all have weight -1 - L.

theorem Zeta32.Outer.Scl_low {n p c : ℕ} (h73 : 7 * n < 3 * p) (hc : c + 1 ≤ n) : (-if c < 5 * n - 2 * p then 1 else 0) ≤ Scl n p c

Class 1 ≤ ρ ≤ n (c + 1 ≤ n): the node ρ is cancelled, the T ≤ 2 others have weight 1 - T.

theorem Zeta32.Outer.Scl_high {n p c : ℕ} (h73 : 7 * n < 3 * p) (hp5 : p ≤ 5 * n) (hc1 : n < c + 1) (hc2 : c + 1 < p) : (-4 * if c < 5 * n - p then 1 else 0) ≤ Scl n p c

Class n < ρ < p: T ≤ 1 nodes of weight -T - 3 and the node ρ < p of weight -T.