The inner-range weights (4.6)–(4.7) and their validity

With class constants b a = Bse p K N a, dimensions L, and top a = L a + (b a - 4)/2:

• w (a, i) = i + (b a - 4)/2 for a ≠ 0;
• w (0, i) = min (2 i + (b 0 - 4)/2) (min_{c ≠ 0} top c). If top a - 1 ≤ top c for all a, c ≠ 0 (P) and top a - 1 ≤ 2 L 0 + (b 0 - 4)/2 for a ≠ 0 (Z), then v_p^G(Δ) ≥ 2 ∑ w.

noncomputable def Zeta5Irrational.topw {m : ℕ} (L : Fin (m + 1) → ℕ) (b : ℕ → ℚ) (a : Fin (m + 1)) : ℚ

top a = L a + (b a - 4)/2.

Equations

• Zeta5Irrational.topw L b a = ↑(L a) + (b ↑a - 4) / 2

noncomputable def Zeta5Irrational.tmin {m : ℕ} (hm : 1 ≤ m) (L : Fin (m + 1) → ℕ) (b : ℕ → ℚ) : ℚ

The minimum of top over the ordinary classes.

Equations

• Zeta5Irrational.tmin hm L b = (Finset.univ.erase 0).inf' ⋯ (Zeta5Irrational.topw L b)

theorem Zeta5Irrational.tmin_le {m : ℕ} (hm : 1 ≤ m) (L : Fin (m + 1) → ℕ) (b : ℕ → ℚ) {c : Fin (m + 1)} (hc : c ≠ 0) : tmin hm L b ≤ topw L b c

noncomputable def Zeta5Irrational.winner {m : ℕ} (hm : 1 ≤ m) (L : Fin (m + 1) → ℕ) (b : ℕ → ℚ) (s : (a : Fin (m + 1)) × Fin (L a)) : ℚ

The weights.

Equations

• Zeta5Irrational.winner hm L b s = if s.fst = 0 then min (2 * ↑↑s.snd + (b 0 - 4) / 2) (Zeta5Irrational.tmin hm L b) else ↑↑s.snd + (b ↑s.fst - 4) / 2

theorem Zeta5Irrational.winner_ACI {m : ℕ} (hm : 1 ≤ m) (L : Fin (m + 1) → ℕ) (b : ℕ → ℚ) (hP : ∀ (a c : Fin (m + 1)), a ≠ 0 → c ≠ 0 → topw L b a - 1 ≤ topw L b c) (hZ : ∀ (a : Fin (m + 1)), a ≠ 0 → topw L b a - 1 ≤ 2 * ↑(L 0) + (b 0 - 4) / 2) (s t : (a : Fin (m + 1)) × Fin (L a)) (a : Fin (m + 1)) : winner hm L b s + winner hm L b t + 4 ≤ b ↑a + (if a = 0 then 2 else 1) * (↑(nu L s a) + ↑(nu L t a))

The abstract class inequality.

theorem Zeta5Irrational.inner_bound {m p : ℕ} [Fact (Nat.Prime p)] (hp5 : 5 ≤ p) (hm : 2 * m + 1 = p) (hm1 : 1 ≤ m) (n : ℕ) (L : Fin (m + 1) → ℕ) (hL : ∑ c : Fin (m + 1), L c = 37 * n) (hsep : Sep p (PlK (40 * n))) (hK : 40 * n < p ^ 2) (hdeg : 5 + 2 * (18 * n + 2 * (37 * n)) - 2 * (40 * n) + 1 < p ^ 2) (hP : ∀ (a c : Fin (m + 1)), a ≠ 0 → c ≠ 0 → topw L (Bse p (40 * n) (3 * n)) a - 1 ≤ topw L (Bse p (40 * n) (3 * n)) c) (hZ : ∀ (a : Fin (m + 1)), a ≠ 0 → topw L (Bse p (40 * n) (3 * n)) a - 1 ≤ 2 * ↑(L 0) + (Bse p (40 * n) (3 * n) 0 - 4) / 2) : GV p (Δ n) (2 * ∑ s : (a : Fin (m + 1)) × Fin (L a), winner hm1 L (Bse p (40 * n) (3 * n)) s)

Inner-range determinant bound for an allocation satisfying (P) and (Z).

Capped weights: validity needs only the zero-class condition

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

Uncapped weights.

Equations

• Zeta5Irrational.wraw L b s = if s.fst = 0 then 2 * ↑↑s.snd + (b 0 - 4) / 2 else ↑↑s.snd + (b ↑s.fst - 4) / 2

noncomputable def Zeta5Irrational.wcap {m : ℕ} (hm : 1 ≤ m) (L : Fin (m + 1) → ℕ) (b : ℕ → ℚ) (s : (a : Fin (m + 1)) × Fin (L a)) : ℚ

Capped weights min (wraw) (min_{c ≠ 0} top c).

Equations

• Zeta5Irrational.wcap hm L b s = min (Zeta5Irrational.wraw L b s) (Zeta5Irrational.tmin hm L b)

theorem Zeta5Irrational.wcap_ACI {m : ℕ} (hm : 1 ≤ m) (L : Fin (m + 1) → ℕ) (b : ℕ → ℚ) (hZ : tmin hm L b ≤ 2 * ↑(L 0) + (b 0 - 4) / 2) (s t : (a : Fin (m + 1)) × Fin (L a)) (a : Fin (m + 1)) : wcap hm L b s + wcap hm L b t + 4 ≤ b ↑a + (if a = 0 then 2 else 1) * (↑(nu L s a) + ↑(nu L t a))

theorem Zeta5Irrational.inner_bound_cap {m p : ℕ} [Fact (Nat.Prime p)] (hp5 : 5 ≤ p) (hm : 2 * m + 1 = p) (hm1 : 1 ≤ m) (n : ℕ) (L : Fin (m + 1) → ℕ) (hL : ∑ c : Fin (m + 1), L c = 37 * n) (hsep : Sep p (PlK (40 * n))) (hK : 40 * n < p ^ 2) (hdeg : 5 + 2 * (18 * n + 2 * (37 * n)) - 2 * (40 * n) + 1 < p ^ 2) (hZ : tmin hm1 L (Bse p (40 * n) (3 * n)) ≤ 2 * ↑(L 0) + (Bse p (40 * n) (3 * n) 0 - 4) / 2) : GV p (Δ n) (2 * ∑ s : (a : Fin (m + 1)) × Fin (L a), wcap hm1 L (Bse p (40 * n) (3 * n)) s)

Inner-range determinant bound with capped weights; only the zero-class condition.