Outer range: general residue and pole-value lemmas

For a numerator tpol M = ∏_{γ ∈ M} (t + γ²):

• res_tpol : res K (tpol M) j = ∏_γ (γ² - j²) / ∏_{i ≠ j} (i² - j²);
• valuation bounds for residues and pole values;
• PV_congr : poleValue (p - c) ≡ poleValue c (mod p).

theorem Zeta5Irrational.eval_tpol (M : Multiset ℤ) (x : ℚ) : Polynomial.eval x (tpol M) = (Multiset.map (fun (γ : ℤ) => x + ↑γ ^ 2) M).prod

theorem Zeta5Irrational.res_tpol {K j : ℕ} (hj : j ∈ Finset.Icc 1 K) (M : Multiset ℤ) : res K (tpol M) j = (Multiset.map (fun (γ : ℤ) => ↑γ ^ 2 - ↑j ^ 2) M).prod / ∏ i ∈ (Finset.Icc 1 K).erase j, (↑i ^ 2 - ↑j ^ 2)

theorem Zeta5Irrational.res_tpol_eq_zero {K j : ℕ} (hj : j ∈ Finset.Icc 1 K) {M : Multiset ℤ} {γ : ℤ} (hγ : γ ∈ M) (h : γ ^ 2 = ↑j ^ 2) : res K (tpol M) j = 0

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

The numerator valuation: at least the number of roots γ with γ² ≡ j².

theorem Zeta5Irrational.padicValRat_den_le {p : ℕ} [hp : Fact (Nat.Prime p)] (hp3 : 3 ≤ 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))) ≤ ↑{i ∈ (Finset.Icc 1 K).erase j | ↑↑i ^ 2 = ↑↑j ^ 2}.card

The denominator valuation for a nonzero class: at most the number of other nodes in the class (each factor has valuation ≤ 1).