the proof notes, §6: the greedy layout for n = p - 1, layout (4,5,3).

Classes b ∈ {0, …, p-1} of the disc t = -b + p u:

• zero class b = 0: column base c_0 = -5, multiplicity 4, levels -5, -3, -1, 1;
• low classes 1 ≤ b ≤ p-5 (b + 5 ≤ p): c_b = -3, multiplicity 3, levels -3, -1, 1;
• high classes p-4 ≤ b ≤ p-1: c_b = -2, multiplicity 2, levels -2, 0.

A basis vector is a = ⟨b, i⟩ : Idx p with i < mult p b; its greedy level is level a = c_b + 2 i and its weight is rho a = level a / 2. kmul a d is the multiplicity of (t + d) in the CRT basis vector a, and discExp a c d = c_d + kmul a d + kmul c d is the Lemma 4 exponent of the entry (a, c) on disc d.

def Zeta32.PrimeEdge.mult (p b : ℕ) : ℕ

Multiplicity m_b of the class b in the CRT basis.

Equations

• Zeta32.PrimeEdge.mult p b = if b = 0 then 4 else if b + 5 ≤ p then 3 else 2

def Zeta32.PrimeEdge.colBase (p b : ℕ) : ℤ

Greedy column base c_b = s N_b - C_b + [b = 0] - 2 for n = p - 1.

Equations

• Zeta32.PrimeEdge.colBase p b = if b = 0 then -5 else if b + 5 ≤ p then -3 else -2

@[reducible, inline]

abbrev Zeta32.PrimeEdge.Idx (p : ℕ) : Type

Basis index: a class b and an order i < m_b.

Equations

• Zeta32.PrimeEdge.Idx p = ((b : Fin p) × Fin (Zeta32.PrimeEdge.mult p ↑b))

def Zeta32.PrimeEdge.level (p : ℕ) (a : Idx p) : ℤ

Greedy level π_a = c_b + 2 i.

Equations

• Zeta32.PrimeEdge.level p a = Zeta32.PrimeEdge.colBase p ↑a.fst + 2 * ↑↑a.snd

def Zeta32.PrimeEdge.rho (p : ℕ) (a : Idx p) : ℚ

Row/column weight ρ_a = π_a / 2.

Equations

• Zeta32.PrimeEdge.rho p a = ↑(Zeta32.PrimeEdge.level p a) / 2

def Zeta32.PrimeEdge.kmul (p : ℕ) (a : Idx p) (d : ℕ) : ℕ

Multiplicity of (t + d) in the basis vector a.

Equations

• Zeta32.PrimeEdge.kmul p a d = if ↑a.fst = d then ↑a.snd else Zeta32.PrimeEdge.mult p d

def Zeta32.PrimeEdge.discExp (p : ℕ) (a c : Idx p) (d : ℕ) : ℤ

Lemma 4 exponent of the entry (a, c) on the disc d.

Equations

• Zeta32.PrimeEdge.discExp p a c d = Zeta32.PrimeEdge.colBase p d + ↑(Zeta32.PrimeEdge.kmul p a d) + ↑(Zeta32.PrimeEdge.kmul p c d)

theorem Zeta32.PrimeEdge.sum_mult {p : ℕ} (hp : 5 ≤ p) : ∑ b ∈ Finset.range p, mult p b = 3 * (p - 1)

theorem Zeta32.PrimeEdge.card_Idx {p : ℕ} (hp : 5 ≤ p) : Fintype.card (Idx p) = 3 * (p - 1)

theorem Zeta32.PrimeEdge.level_le_one {p : ℕ} (a : Idx p) : level p a ≤ 1

theorem Zeta32.PrimeEdge.two_le_colBase_add_mult {p : ℕ} (d : ℕ) : 2 ≤ colBase p d + 2 * ↑(mult p d)

theorem Zeta32.PrimeEdge.level_le_disc {p : ℕ} (a : Idx p) (d : ℕ) : level p a ≤ colBase p d + 2 * ↑(kmul p a d)

Greedy property: c_d + 2 k_d(a) ≥ π_a on every disc.

theorem Zeta32.PrimeEdge.level_add_le_discExp {p : ℕ} (a c : Idx p) (d : ℕ) : level p a + level p c ≤ 2 * discExp p a c d

theorem Zeta32.PrimeEdge.level_add_lt_discExp {p : ℕ} (a c : Idx p) (hac : a.fst ≠ c.fst) (d : ℕ) : level p a + level p c + 1 ≤ 2 * discExp p a c d

No tie: across two different classes the greedy inequality is strict.

theorem Zeta32.PrimeEdge.rho_add_le_discExp {p : ℕ} (a c : Idx p) (d : ℕ) : rho p a + rho p c ≤ ↑(discExp p a c d)

theorem Zeta32.PrimeEdge.rho_add_half_le_discExp {p : ℕ} (a c : Idx p) (hac : a.fst ≠ c.fst) (d : ℕ) : rho p a + rho p c + 1 / 2 ≤ ↑(discExp p a c d)

theorem Zeta32.PrimeEdge.rho_add_of_same {p : ℕ} (a c : Idx p) (hac : a.fst = c.fst) : rho p a + rho p c = ↑(colBase p ↑a.fst + ↑↑a.snd + ↑↑c.snd)

Same class b: ρ_a + ρ_c = c_b + i + k, an integer.