Outer range: entry bounds

Helper lemmas (memberships, root counts, zero-class valuations).

def Zeta5Irrational.entryO {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (n : ℕ) (cs : Fin (m + 1)) (is : ℕ) (ct : Fin (m + 1)) (it : ℕ) : Multiset ℤ

The entry roots 6·[1..N] + rows.

Equations

• Zeta5Irrational.entryO hm n cs is ct it = 6 • Multiset.map (fun (j : ℕ) => ↑j) (Finset.Icc 1 (3 * n)).val + Zeta5Irrational.rootsO hm n cs is + Zeta5Irrational.rootsO hm n ct it

theorem Zeta5Irrational.mem_entryO_small {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (n : ℕ) {cs ct : Fin (m + 1)} {is it k : ℕ} (hk : k ∈ Finset.Icc 1 (3 * n)) : ↑k ∈ entryO hm n cs is ct it

theorem Zeta5Irrational.mem_rootsO_other {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (n : ℕ) {c : Fin (m + 1)} {i j : ℕ} (hj : j ∈ tailO n) (hc : jc hm j ≠ c) : ↑j ∈ rootsO hm n c i

theorem Zeta5Irrational.mem_rootsO_big {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (n : ℕ) {c : Fin (m + 1)} {i j : ℕ} (hi : nbC hm n c ≤ i) (hj : j ∈ bigC hm n c) : ↑j ∈ rootsO hm n c i

theorem Zeta5Irrational.mem_entryO_left {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (n : ℕ) {cs ct : Fin (m + 1)} {is it : ℕ} {γ : ℤ} (h : γ ∈ rootsO hm n cs is) : γ ∈ entryO hm n cs is ct it

theorem Zeta5Irrational.mem_entryO_right {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (n : ℕ) {cs ct : Fin (m + 1)} {is it : ℕ} {γ : ℤ} (h : γ ∈ rootsO hm n ct it) : γ ∈ entryO hm n cs is ct it

theorem Zeta5Irrational.count_rootsO {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (n : ℕ) (c : Fin (m + 1)) (i : ℕ) (x : ZMod p) (hx : x ^ 2 = ↑↑↑c ^ 2) : i ≤ (Multiset.filter (fun (γ : ℤ) => ↑γ ^ 2 = x ^ 2) (rootsO hm n c i)).card

Count of roots in the class of c in a row of class c.

theorem Zeta5Irrational.VG_prod_sq_sub_zero {p : ℕ} [hp : Fact (Nat.Prime p)] (M : Multiset ℤ) {j : ℤ} (hj : ↑p ∣ j) : VG p (Multiset.map (fun (γ : ℤ) => ↑γ ^ 2 - ↑j ^ 2) M).prod (2 * ↑(Multiset.filter (fun (γ : ℤ) => ↑p ∣ γ) M).card)

The valuation of ∏ (γ² - j²) for p ∣ j: two per root divisible by p.

theorem Zeta5Irrational.padicValRat_den_zero_le {p : ℕ} [hp : Fact (Nat.Prime p)] {K j : ℕ} (hj : j ∈ Finset.Icc 1 K) (hK : 2 * K < p ^ 2) (hj0 : ↑p ∣ ↑j) : ↑(padicValRat p (∏ i ∈ (Finset.Icc 1 K).erase j, (↑i ^ 2 - ↑j ^ 2))) ≤ 2 * ↑{i ∈ (Finset.Icc 1 K).erase j | ↑p ∣ ↑i}.card

Denominator for p ∣ j: at most two per other multiple of p.

theorem Zeta5Irrational.VG_res_class {p : ℕ} [hp : Fact (Nat.Prime p)] (hp3 : 3 ≤ p) {K : ℕ} (hK : 2 * K < p ^ 2) (M : Multiset ℤ) {j : ℕ} (hj : j ∈ Finset.Icc 1 K) (hj0 : ¬↑p ∣ ↑j) : VG p (res K (tpol M) j) (↑(Multiset.filter (fun (γ : ℤ) => ↑γ ^ 2 = ↑↑j ^ 2) M).card - ↑{i ∈ (Finset.Icc 1 K).erase j | ↑↑i ^ 2 = ↑↑j ^ 2}.card)

Residue bound for a nonzero class.

theorem Zeta5Irrational.eval_sub_eval_int {p : ℕ} [hp : Fact (Nat.Prime p)] {S : Polynomial ℚ} (hS : GV p S 0) {u v : ℚ} (hu : VG p u 0) (hv : VG p v 0) : ∃ (T : ℚ), Polynomial.eval u S - Polynomial.eval v S = (u - v) * T ∧ VG p T 0

Divided differences of integral polynomials are integral.

theorem Zeta5Irrational.GV_tpol {p : ℕ} (M : Multiset ℤ) : GV p (tpol M) 0

theorem Zeta5Irrational.sq_ne_of_ne {i j : ℕ} (h : i ≠ j) : ↑i ^ 2 - ↑j ^ 2 ≠ 0

theorem Zeta5Irrational.pair_GV {p : ℕ} [hp : Fact (Nat.Prime p)] (hp3 : 3 ≤ p) {K : ℕ} (M : Multiset ℤ) {a : ℕ} (ha1 : 1 ≤ a) (hap : a < p) (hne : a ≠ p - a) (haK : a ≤ K) (hbK : p - a ≤ K) (hroots : ∀ i ∈ Finset.Icc 1 K, i ≠ a → i ≠ p - a → ↑i ∈ M) (hres : VG p (res K (tpol M) (p - a)) (-1)) : GV p (Polynomial.C (res K (tpol M) a) * poleValue a + Polynomial.C (res K (tpol M) (p - a)) * poleValue (p - a)) 0

The pairing lemma: two remaining poles a, p - a give an integral contribution.