The class-basis framework

Classes a = 0, …, m (with p = 2m + 1), dimensions L a with ∑ L = h, basis polynomials E_{a,i} = ∏_{c ≠ a} (t + c²)^{L_c} (t + a²)^i (i < L a). If weights w satisfy the per-class entry inequalities, then v_p^G(Δ) ≥ 2 ∑ w.

def Zeta5Irrational.classRoots {m : ℕ} (L : Fin (m + 1) → ℕ) (a : Fin (m + 1)) (i : ℕ) : Multiset ℤ

The t-roots of the basis polynomial E_{a,i}.

Equations

• Zeta5Irrational.classRoots L a i = ∑ c ∈ Finset.univ.erase a, Multiset.replicate (L c) ↑↑c + Multiset.replicate i ↑↑a

theorem Zeta5Irrational.card_classRoots {m : ℕ} (L : Fin (m + 1) → ℕ) (a : Fin (m + 1)) (i : ℕ) : (classRoots L a i).card = ∑ c ∈ Finset.univ.erase a, L c + i

noncomputable def Zeta5Irrational.tpolZ (M : Multiset ℤ) : Polynomial ℤ

∏_{γ ∈ M} (t + γ²) over ℤ.

Equations

• Zeta5Irrational.tpolZ M = (Multiset.map (fun (γ : ℤ) => Polynomial.X + Polynomial.C (γ ^ 2)) M).prod

theorem Zeta5Irrational.tpolZ_map_Q (M : Multiset ℤ) : Polynomial.map (Int.castRingHom ℚ) (tpolZ M) = tpol M

theorem Zeta5Irrational.natDegree_tpolZ (M : Multiset ℤ) : (tpolZ M).natDegree ≤ M.card

theorem Zeta5Irrational.prod_map_sum_replicate {α : Type u_1} {β : Type u_2} [CommMonoid β] (s : Finset α) (L : α → ℕ) (v : α → ℤ) (g : ℤ → β) : (Multiset.map g (∑ c ∈ s, Multiset.replicate (L c) (v c))).prod = ∏ c ∈ s, g (v c) ^ L c

theorem Zeta5Irrational.tpolZ_map_ZMod (p : ℕ) {m : ℕ} (L : Fin (m + 1) → ℕ) (a : Fin (m + 1)) (i : ℕ) : Polynomial.map (Int.castRingHom (ZMod p)) (tpolZ (classRoots L a i)) = (∏ c ∈ Finset.univ.erase a, (Polynomial.X - Polynomial.C (-↑↑c ^ 2)) ^ L c) * (Polynomial.X - Polynomial.C (-↑↑a ^ 2)) ^ i

theorem Zeta5Irrational.D_eq_tpol (m : ℕ) : D m = tpol (Multiset.map (fun (j : ℕ) => ↑j) (Finset.Icc 1 m).val)

D_m as a tpol.

theorem Zeta5Irrational.tpol_nsmul (k : ℕ) (M : Multiset ℤ) : tpol (k • M) = tpol M ^ k

theorem Zeta5Irrational.sq_injective {p m : ℕ} [hp : Fact (Nat.Prime p)] (hm : 2 * m + 1 = p) : Function.Injective fun (c : Fin (m + 1)) => -↑↑c ^ 2

The squares of 0, …, m are distinct modulo p = 2m + 1.

def Zeta5Irrational.entryRoots {m : ℕ} (N : ℕ) (L : Fin (m + 1) → ℕ) (s t : (a : Fin (m + 1)) × Fin (L a)) : Multiset ℤ

The t-roots of the numerator D_N⁶ E_s E_t.

Equations

• Zeta5Irrational.entryRoots N L s t = 6 • Multiset.map (fun (j : ℕ) => ↑j) (Finset.Icc 1 N).val + Zeta5Irrational.classRoots L s.fst ↑s.snd + Zeta5Irrational.classRoots L t.fst ↑t.snd

noncomputable def Zeta5Irrational.classCount (p K : ℕ) (M : Multiset ℤ) (c : ZMod p) : ℚ

The per-class count appearing in the entry bound.

Equations

• One or more equations did not get rendered due to their size.

theorem Zeta5Irrational.class_frame {p : ℕ} [hp : Fact (Nat.Prime p)] (hp5 : 5 ≤ p) {m : ℕ} (hm : 2 * m + 1 = p) (n : ℕ) (L : Fin (m + 1) → ℕ) (hL : ∑ c : Fin (m + 1), L c = 37 * n) (w : (a : Fin (m + 1)) × Fin (L a) → ℚ) (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) (hentry : ∀ (s t : (a : Fin (m + 1)) × Fin (L a)) (c : ZMod p), w s + w t + 4 ≤ classCount p (40 * n) (entryRoots (3 * n) L s t) c) : GV p (Δ n) (2 * ∑ s : (a : Fin (m + 1)) × Fin (L a), w s)

The class-basis framework: v_p^G(Δ) ≥ 2 ∑ w.