Class counting

For p = 2m + 1 every residue c mod p is ≡ ±a for a unique a ∈ {0, …, m} (ccls c). We express the per-class counts classCount of the framework in terms of these classes.

def Zeta5Irrational.mu (p a : ℕ) (c : ZMod p) : ℕ

μ(a, c) = [a ≡ c] + [a ≡ -c].

Equations

• Zeta5Irrational.mu p a c = (if ↑↑a = c then 1 else 0) + if ↑↑a = -c then 1 else 0

def Zeta5Irrational.ccls {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (c : ZMod p) : Fin (m + 1)

The class of a residue.

Equations

• Zeta5Irrational.ccls hm c = if h : c.val ≤ m then ⟨c.val, ⋯⟩ else ⟨p - c.val, ⋯⟩

theorem Zeta5Irrational.ccls_spec {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (c : ZMod p) : ↑↑↑(ccls hm c) = c ∨ ↑↑↑(ccls hm c) = -c

theorem Zeta5Irrational.two_ne_zero_zmod {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) : 2 ≠ 0

theorem Zeta5Irrational.ccls_unique {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (c : ZMod p) (a : Fin (m + 1)) (h : ↑↑↑a = c ∨ ↑↑↑a = -c) : a = ccls hm c

Uniqueness of the class.

theorem Zeta5Irrational.mu_eq {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (a : Fin (m + 1)) (c : ZMod p) : mu p (↑a) c = if a = ccls hm c then if c = 0 then 2 else 1 else 0

def Zeta5Irrational.SX (p X : ℕ) (c : ZMod p) : ℕ

#{j ≤ X : j ≡ c} + #{j ≤ X : j ≡ -c}.

Equations

• Zeta5Irrational.SX p X c = {j ∈ Finset.Icc 1 X | ↑↑j = c}.card + {j ∈ Finset.Icc 1 X | ↑↑j = -c}.card

theorem Zeta5Irrational.SX_neg {p : ℕ} [hp : Fact (Nat.Prime p)] (X : ℕ) (c : ZMod p) : SX p X (-c) = SX p X c

theorem Zeta5Irrational.SX_ccls {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (X : ℕ) (c : ZMod p) : SX p X c = SX p X ↑↑↑(ccls hm c)

noncomputable def Zeta5Irrational.Bse (p K N a : ℕ) : ℚ

The class constant 5[a = 0] + 6 S_N(a) - S_K(a).

Equations

• Zeta5Irrational.Bse p K N a = (if a = 0 then 5 else 0) + 6 * ↑(Zeta5Irrational.SX p N ↑↑a) - ↑(Zeta5Irrational.SX p K ↑↑a)

def Zeta5Irrational.nu {m : ℕ} (L : Fin (m + 1) → ℕ) (s : (a : Fin (m + 1)) × Fin (L a)) (b : Fin (m + 1)) : ℕ

The vanishing order of the row s = (a, i) at the class b.

Equations

• Zeta5Irrational.nu L s b = if b = s.fst then ↑s.snd else L b

theorem Zeta5Irrational.card_filter_replicate (k : ℕ) (v : ℤ) (P : ℤ → Prop) [DecidablePred P] : (Multiset.filter P (Multiset.replicate k v)).card = if P v then k else 0

theorem Zeta5Irrational.card_filter_sum_replicate {α : Type u_1} (s : Finset α) (L : α → ℕ) (v : α → ℤ) (P : ℤ → Prop) [DecidablePred P] : (Multiset.filter P (∑ c ∈ s, Multiset.replicate (L c) (v c))).card = ∑ c ∈ s, if P (v c) then L c else 0

theorem Zeta5Irrational.count_classRoots {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (L : Fin (m + 1) → ℕ) (s : (a : Fin (m + 1)) × Fin (L a)) (c : ZMod p) : (Multiset.filter (fun (γ : ℤ) => ↑γ = c) (classRoots L s.fst ↑s.snd)).card + (Multiset.filter (fun (γ : ℤ) => ↑γ = -c) (classRoots L s.fst ↑s.snd)).card = (if c = 0 then 2 else 1) * nu L s (ccls hm c)

theorem Zeta5Irrational.count_DN {p : ℕ} [hp : Fact (Nat.Prime p)] (N : ℕ) (c : ZMod p) : (Multiset.filter (fun (γ : ℤ) => ↑γ = c) (6 • Multiset.map (fun (j : ℕ) => ↑j) (Finset.Icc 1 N).val)).card + (Multiset.filter (fun (γ : ℤ) => ↑γ = -c) (6 • Multiset.map (fun (j : ℕ) => ↑j) (Finset.Icc 1 N).val)).card = 6 * SX p N c

theorem Zeta5Irrational.card_plc_PlK {p : ℕ} [hp : Fact (Nat.Prime p)] (K : ℕ) (c : ZMod p) : (plc p (PlK K) c).card = SX p K c

theorem Zeta5Irrational.ccls_eq_zero_iff {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (c : ZMod p) : ccls hm c = 0 ↔ c = 0

theorem Zeta5Irrational.classCount_eq {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (K N : ℕ) (L : Fin (m + 1) → ℕ) (s t : (a : Fin (m + 1)) × Fin (L a)) (c : ZMod p) : classCount p K (entryRoots N L s t) c = Bse p K N ↑(ccls hm c) + (if ccls hm c = 0 then 2 else 1) * (↑(nu L s (ccls hm c)) + ↑(nu L t (ccls hm c)))

The class counts in terms of Bse and the row vanishing orders.