the proof notes end of §4 (used as range R3 in §8): for a prime p > 5n with p ∤ den r, every coefficient of Qtilde r n is p-integral. Every Hankel entry is p-integral (the polynomial-part moments have degree ≤ 5n - 2 ≤ p - 3; for j ≤ 5n < p the residue ρ_j and β_j are p-integral), and the normalizer S_n^{3n}/F_n is a p-adic unit.

theorem Zeta32.Outer.wv_nonneg_large {n p j : ℕ} (hj : j ≤ 5 * n) (h5 : 5 * n < p) : 0 ≤ wv n p j

theorem Zeta32.Outer.normVal_large {n p : ℕ} (h5 : 5 * n < p) : normVal p n = 0

theorem Zeta32.Outer.Q_GV_large {r : ℚ} {n p : ℕ} [hp : Fact (Nat.Prime p)] (h5 : 5 * n < p) (hr : Zeta5Irrational.VG p r 0) : Zeta5Irrational.GV p (Q r n) 0

theorem Zeta32.Arith.large_prime_integrality (r : ℚ) (n p : ℕ) : Nat.Prime p → 5 * n < p → ¬p ∣ r.den → ∀ (k : ℕ), (Qtilde r n).coeff k ≠ 0 → 0 ≤ padicValRat p ((Qtilde r n).coeff k)

the proof notes, §4, last paragraph: for p > 5n, p ∤ den r, every nonzero coefficient of Qtilde r n has nonnegative p-adic valuation.