The greedy allocation (the proof notes, §3)

Columns b < p with entries c_b, c_b + 2, c_b + 4, … (c_b = colVal n p b). At step i take the smallest untaken entry gval i, from column gpick i; galloc i b is the number of entries taken from column b before step i.

• sum_galloc : ∑_{b<p} galloc i b = i;
• allocCost_galloc : allocCost n p (galloc i) = ∑_{j<i} gval j;
• gval_le : gval i ≤ c_b + 2 galloc i b for every b < p (greedy rule);
• gbasis i = ∏_{b<p} (X + b)^{galloc i b} is monic of degree i, with galloc i b zeros in the class of -b (Adm_gbasis).

theorem Zeta32.Arith.Local.exists_greedy_choice (n p : ℕ) (hp : 0 < p) (κ : ℕ → ℕ) : ∃ b ∈ Finset.range p, ∀ b' ∈ Finset.range p, colVal n p b + 2 * ↑(κ b) ≤ colVal n p b' + 2 * ↑(κ b')

noncomputable def Zeta32.Arith.Local.gchoice (n p : ℕ) (κ : ℕ → ℕ) : ℕ

The greedy choice of a column.

Equations

• Zeta32.Arith.Local.gchoice n p κ = if h : 0 < p then ⋯.choose else 0

noncomputable def Zeta32.Arith.Local.galloc (n p : ℕ) : ℕ → ℕ → ℕ

The allocation before step i.

Equations

• Zeta32.Arith.Local.galloc n p 0 = fun (x : ℕ) => 0
• Zeta32.Arith.Local.galloc n p i.succ = fun (b : ℕ) => Zeta32.Arith.Local.galloc n p i b + if b = Zeta32.Arith.Local.gchoice n p (Zeta32.Arith.Local.galloc n p i) then 1 else 0

noncomputable def Zeta32.Arith.Local.gpick (n p i : ℕ) : ℕ

The column chosen at step i.

Equations

• Zeta32.Arith.Local.gpick n p i = Zeta32.Arith.Local.gchoice n p (Zeta32.Arith.Local.galloc n p i)

noncomputable def Zeta32.Arith.Local.gval (n p i : ℕ) : ℤ

The entry taken at step i.

Equations

• Zeta32.Arith.Local.gval n p i = Zeta32.colVal n p (Zeta32.Arith.Local.gpick n p i) + 2 * ↑(Zeta32.Arith.Local.galloc n p i (Zeta32.Arith.Local.gpick n p i))

theorem Zeta32.Arith.Local.galloc_succ (n p i b : ℕ) : galloc n p (i + 1) b = galloc n p i b + if b = gpick n p i then 1 else 0

theorem Zeta32.Arith.Local.gpick_mem {n p : ℕ} (hp : 0 < p) (i : ℕ) : gpick n p i ∈ Finset.range p

theorem Zeta32.Arith.Local.gval_le {n p : ℕ} (hp : 0 < p) (i : ℕ) {b : ℕ} (hb : b ∈ Finset.range p) : gval n p i ≤ colVal n p b + 2 * ↑(galloc n p i b)

theorem Zeta32.Arith.Local.sum_galloc {n p : ℕ} (hp : 0 < p) (i : ℕ) : ∑ b ∈ Finset.range p, galloc n p i b = i

theorem Zeta32.Arith.Local.allocCost_galloc {n p : ℕ} (hp : 0 < p) (i : ℕ) : allocCost n p (galloc n p i) = ∑ j ∈ Finset.range i, gval n p j

The basis

noncomputable def Zeta32.Arith.Local.gbasis (n p i : ℕ) : Polynomial ℚ

∏_{b<p} (X + b)^{galloc i b}.

Equations

• Zeta32.Arith.Local.gbasis n p i = ∏ b ∈ Finset.range p, (Polynomial.X + Polynomial.C ↑b) ^ Zeta32.Arith.Local.galloc n p i b

theorem Zeta32.Arith.Local.gbasis_monic {n p : ℕ} (i : ℕ) : (gbasis n p i).Monic

theorem Zeta32.Arith.Local.gbasis_natDegree {n p : ℕ} (hp : 0 < p) (i : ℕ) : (gbasis n p i).natDegree = i

Class counts

theorem Zeta32.Arith.Local.X_add_C_eq (b : ℕ) : Polynomial.X + Polynomial.C ↑b = Polynomial.X - Polynomial.C ↑(-↑b)

theorem Zeta32.Arith.Local.Adm.X_add_C {p : ℕ} [hp : Fact (Nat.Prime p)] (b : ℕ) : Adm p (Polynomial.X + Polynomial.C ↑b) fun (c : ZMod p) => if ↑(-↑b) = c then 1 else 0

theorem Zeta32.Arith.Local.neg_class_iff {p : ℕ} [hp : Fact (Nat.Prime p)] (j : ℕ) (c : ZMod p) : ↑(-↑j) = c ↔ j % p = (-c).val

theorem Zeta32.Arith.Local.neg_val_lt {p : ℕ} [hp : Fact (Nat.Prime p)] (c : ZMod p) : (-c).val ∈ Finset.range p

theorem Zeta32.Arith.Local.neg_val_eq_zero_iff {p : ℕ} [hp : Fact (Nat.Prime p)] (c : ZMod p) : (-c).val = 0 ↔ c = 0

theorem Zeta32.Arith.Local.card_class {p : ℕ} [hp : Fact (Nat.Prime p)] (m : ℕ) (c : ZMod p) : {j ∈ Finset.Icc 1 m | ↑(-↑j) = c}.card = {j ∈ Finset.Icc 1 m | j % p = (-c).val}.card

theorem Zeta32.Arith.Local.Adm_gbasis {n p : ℕ} [hp : Fact (Nat.Prime p)] (i : ℕ) : Adm p (gbasis n p i) fun (c : ZMod p) => ↑(galloc n p i (-c).val)

theorem Zeta32.Arith.Local.Adm_D {p : ℕ} [hp : Fact (Nat.Prime p)] (m : ℕ) : Adm p (D m) fun (c : ZMod p) => ↑{j ∈ Finset.Icc 1 m | j % p = (-c).val}.card