the proof notes, §2, Lemma 3 (local integrality) for the finite local functional locValue of Local.lean: linearity in the numerator, the valuation of locValue s (u^e) M for M ⊆ {0,…,4} (≥ -1 always, ≥ 0 if e ≤ |M| + 2p - 2), the s-dependence (≥ 1 if e ≤ |M| + p - 2), and removal of a near pole at 0 against a factor u.

theorem Zeta32.PrimeEdge.nearPoly_monic (M : Finset ℕ) : (∏ m ∈ M, (Polynomial.X + Polynomial.C ↑m)).Monic

theorem Zeta32.PrimeEdge.natDegree_nearPoly (M : Finset ℕ) : (∏ m ∈ M, (Polynomial.X + Polynomial.C ↑m)).natDegree = M.card

Linearity

theorem Zeta32.PrimeEdge.locPoly_add (s : ℚ) (P Q : Polynomial ℚ) : locPoly s (P + Q) = locPoly s P + locPoly s Q

theorem Zeta32.PrimeEdge.locPoly_smul (s c : ℚ) (P : Polynomial ℚ) : locPoly s (c • P) = c * locPoly s P

theorem Zeta32.PrimeEdge.locValue_add (s : ℚ) (S S' : Polynomial ℚ) (M : Finset ℕ) : locValue s (S + S') M = locValue s S M + locValue s S' M

theorem Zeta32.PrimeEdge.locValue_smul (s c : ℚ) (S : Polynomial ℚ) (M : Finset ℕ) : locValue s (c • S) M = c * locValue s S M

theorem Zeta32.PrimeEdge.locValue_C_mul (s c : ℚ) (S : Polynomial ℚ) (M : Finset ℕ) : locValue s (Polynomial.C c * S) M = c * locValue s S M

theorem Zeta32.PrimeEdge.locValue_zero_left (s : ℚ) (M : Finset ℕ) : locValue s 0 M = 0

theorem Zeta32.PrimeEdge.locValue_sum (s : ℚ) (M : Finset ℕ) {ι : Type u_1} (t : Finset ι) (f : ι → Polynomial ℚ) : locValue s (∑ i ∈ t, f i) M = ∑ i ∈ t, locValue s (f i) M

theorem Zeta32.PrimeEdge.locValue_eq_sum (s : ℚ) (S : Polynomial ℚ) (M : Finset ℕ) {N : ℕ} (hN : S.natDegree < N) : locValue s S M = ∑ e ∈ Finset.range N, S.coeff e * locValue s (Polynomial.X ^ e) M

locValue is the coefficientwise combination of its values on monomials.

Integrality of the pieces

theorem Zeta32.PrimeEdge.GV_X_pow_divByMonic {p : ℕ} (M : Finset ℕ) (e : ℕ) : Zeta5Irrational.GV p (Polynomial.X ^ e /ₘ ∏ m ∈ M, (Polynomial.X + Polynomial.C ↑m)) 0

u^e /ₘ ∏ (u + m) has integer coefficients.

theorem Zeta32.PrimeEdge.padicValRat_diff_eq_zero {p : ℕ} [Fact (Nat.Prime p)] (hp : 5 ≤ p) {m m' : ℕ} (hm : m < 5) (hm' : m' < 5) (hne : m' ≠ m) : ↑m' - ↑m ≠ 0 ∧ padicValRat p (↑m' - ↑m) = 0

theorem Zeta32.PrimeEdge.prod_diff_unit {p : ℕ} [Fact (Nat.Prime p)] (hp : 5 ≤ p) {M : Finset ℕ} (hM : M ⊆ Finset.range 5) {m : ℕ} (hm : m ∈ M) : ∏ m' ∈ M.erase m, (↑m' - ↑m) ≠ 0 ∧ padicValRat p (∏ m' ∈ M.erase m, (↑m' - ↑m)) = 0

theorem Zeta32.PrimeEdge.VG_H_small {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : m < p) (e : ℕ) : Zeta5Irrational.VG p (H e m) 0

theorem Zeta32.PrimeEdge.VG_locPole {p : ℕ} [Fact (Nat.Prime p)] {s : ℚ} (hs : Zeta5Irrational.VG p s 1) {m : ℕ} (hm : m < p) : Zeta5Irrational.VG p (locPole s m) 0

theorem Zeta32.PrimeEdge.VG_locPole_sub {p : ℕ} [Fact (Nat.Prime p)] {s : ℚ} (hs : Zeta5Irrational.VG p s 1) {m : ℕ} (hm : m < p) : Zeta5Irrational.VG p (locPole s m - locPole 0 m) 1

theorem Zeta32.PrimeEdge.VG_res_X_pow {p : ℕ} [Fact (Nat.Prime p)] (hp : 5 ≤ p) {M : Finset ℕ} (hM : M ⊆ Finset.range 5) {m : ℕ} (hm : m ∈ M) (e : ℕ) : Zeta5Irrational.VG p (Polynomial.eval (-↑m) (Polynomial.X ^ e) / ∏ m' ∈ M.erase m, (↑m' - ↑m)) 0

The residue coefficient (-m)^e / ∏_{m' ≠ m} (m' - m) is integral.

theorem Zeta32.PrimeEdge.VG_locPoly_of {p : ℕ} {s : ℚ} [Fact (Nat.Prime p)] {q : Polynomial ℚ} (hq : Zeta5Irrational.GV p q 0) {r : ℚ} (hb : ∀ j ∈ q.support, Zeta5Irrational.VG p (locMoment s j) r) : Zeta5Irrational.VG p (locPoly s q) r

theorem Zeta32.PrimeEdge.natDegree_X_pow_divByMonic (M : Finset ℕ) (e : ℕ) : (Polynomial.X ^ e /ₘ ∏ m ∈ M, (Polynomial.X + Polynomial.C ↑m)).natDegree = e - M.card

theorem Zeta32.PrimeEdge.VG_locValue_res {p : ℕ} [Fact (Nat.Prime p)] (hp : 5 ≤ p) {s : ℚ} (hs : Zeta5Irrational.VG p s 1) {M : Finset ℕ} (hM : M ⊆ Finset.range 5) (e : ℕ) : Zeta5Irrational.VG p (∑ m ∈ M, (Polynomial.eval (-↑m) (Polynomial.X ^ e) / ∏ m' ∈ M.erase m, (↑m' - ↑m)) * locPole s m) 0

theorem Zeta32.PrimeEdge.VG_locValue_X_pow {p : ℕ} [Fact (Nat.Prime p)] (hp : 5 ≤ p) {s : ℚ} (hs : Zeta5Irrational.VG p s 1) {M : Finset ℕ} (hM : M ⊆ Finset.range 5) (e : ℕ) : Zeta5Irrational.VG p (locValue s (Polynomial.X ^ e) M) (-1)

Lemma 3, monomial form, weak part: v_p(V(u^e / ∏ (u + m))) ≥ -1.

theorem Zeta32.PrimeEdge.VG_locValue_X_pow_zero {p : ℕ} [Fact (Nat.Prime p)] (hp : 5 ≤ p) {s : ℚ} (hs : Zeta5Irrational.VG p s 1) {M : Finset ℕ} (hM : M ⊆ Finset.range 5) {e : ℕ} (he : e + 2 ≤ M.card + 2 * p) : Zeta5Irrational.VG p (locValue s (Polynomial.X ^ e) M) 0

Lemma 3, monomial form: V(u^e / ∏ (u + m)) is integral for e ≤ |M| + 2p - 2.

theorem Zeta32.PrimeEdge.VG_locValue_X_pow_sub {p : ℕ} [Fact (Nat.Prime p)] (hp : 5 ≤ p) {s : ℚ} (hs : Zeta5Irrational.VG p s 1) {M : Finset ℕ} (hM : M ⊆ Finset.range 5) {e : ℕ} (he : e + 2 ≤ M.card + p) : Zeta5Irrational.VG p (locValue s (Polynomial.X ^ e) M - locValue 0 (Polynomial.X ^ e) M) 1

The s-dependence of V(u^e / ∏ (u + m)) is ≡ 0 mod p for e ≤ |M| + p - 2.

A near pole at 0 against a factor u

theorem Zeta32.PrimeEdge.X_mul_divByMonic_X_mul {S T : Polynomial ℚ} (hT : T.Monic) : Polynomial.X * S /ₘ (Polynomial.X * T) = S /ₘ T

theorem Zeta32.PrimeEdge.locValue_X_mul_insert_zero (s : ℚ) (S : Polynomial ℚ) {M : Finset ℕ} (h0 : 0 ∉ M) : locValue s (Polynomial.X * S) (insert 0 M) = locValue s S M