the proof notes, §2 Lemma 3 for truncated scaled numerators, and the coefficients of seriesPart when dissectNum = p^E u^E R: the coefficient of u^e vanishes for e < E and has valuation ≥ e.

theorem Zeta32.PrimeEdge.VG_pow_nat {p : ℕ} [Fact (Nat.Prime p)] (E : ℕ) : Zeta5Irrational.VG p (↑p ^ E) ↑E

theorem Zeta32.PrimeEdge.VG_locValue_scaled {p : ℕ} [Fact (Nat.Prime p)] (hp : 5 ≤ p) {s : ℚ} (hs : Zeta5Irrational.VG p s 1) {M : Finset ℕ} (hM : M ⊆ Finset.range 5) {S : Polynomial ℚ} {E₀ : ℕ} (hS : ∀ (e : ℕ), Zeta5Irrational.VG p (S.coeff e) ↑e) (hz : ∀ e < E₀, S.coeff e = 0) (hE : E₀ + 2 ≤ M.card + 2 * p) : Zeta5Irrational.VG p (locValue s S M) ↑E₀

Lemma 3 (local integrality), scaled form. If the coefficient of u^e in S has valuation ≥ e and vanishes for e < E₀, then V(S / ∏_{m ∈ M} (u + m)) has valuation ≥ E₀, provided E₀ ≤ |M| + 2p - 2.

noncomputable def Zeta32.PrimeEdge.regPart (n p b : ℕ) (R : Polynomial ℚ) : PowerSeries ℚ

The regular part R / farProd as a power series.

Equations

• Zeta32.PrimeEdge.regPart n p b R = ↑R * (↑(Zeta32.PrimeEdge.farProd n p b))⁻¹

theorem Zeta32.PrimeEdge.coeff_seriesPart {p n b : ℕ} {A R : Polynomial ℚ} {E : ℕ} (hA : dissectNum p b A = Polynomial.C (↑p ^ E) * Polynomial.X ^ E * R) (e : ℕ) : (seriesPart n p b A).coeff e = if e < truncOrder n then if E ≤ e then ↑p ^ E * (PowerSeries.coeff (e - E)) (regPart n p b R) else 0 else 0

theorem Zeta32.PrimeEdge.seriesPart_coeff_VG {p : ℕ} [Fact (Nat.Prime p)] {n b : ℕ} {A R : Polynomial ℚ} {E : ℕ} (hA : dissectNum p b A = Polynomial.C (↑p ^ E) * Polynomial.X ^ E * R) (hK : ScaledPS p (regPart n p b R)) (e : ℕ) : Zeta5Irrational.VG p ((seriesPart n p b A).coeff e) ↑e

theorem Zeta32.PrimeEdge.seriesPart_coeff_lt {p n b : ℕ} {A R : Polynomial ℚ} {E : ℕ} (hA : dissectNum p b A = Polynomial.C (↑p ^ E) * Polynomial.X ^ E * R) {e : ℕ} (he : e < E) : (seriesPart n p b A).coeff e = 0

theorem Zeta32.PrimeEdge.seriesPart_coeff_self {p n b : ℕ} {A R : Polynomial ℚ} {E : ℕ} (hA : dissectNum p b A = Polynomial.C (↑p ^ E) * Polynomial.X ^ E * R) (hE : E < truncOrder n) : (seriesPart n p b A).coeff E = ↑p ^ E * (PowerSeries.coeff 0) (regPart n p b R)

theorem Zeta32.PrimeEdge.regPart_scaled {p : ℕ} [Fact (Nat.Prime p)] {n b : ℕ} (hb : b < p) {R : Polynomial ℚ} (hR : Scaled p R) (hR0 : IsUnitV p (R.coeff 0)) : ScaledPS p (regPart n p b R) ∧ IsUnitV p ((PowerSeries.coeff 0) (regPart n p b R))

theorem Zeta32.PrimeEdge.VG_rp {p : ℕ} [hp : Fact (Nat.Prime p)] {r : ℚ} (hr : Zeta5Irrational.VG p r 0) : Zeta5Irrational.VG p (r * ↑p) 1