the proof notes, §7, Lemma 7: crude all-prime coefficient valuation bound. Qtilde r n = det (binomGram r n) (Small/Gram), every entry has Gauss valuation ≥ -3⌊log_p(10n+2)⌋ - v_p(den r) (Small/Entry), and the determinant of a 3n × 3n matrix loses at most 3n times the entry bound (det_GV). Here D = 2h + sn + 2 = 10n + 2.

theorem Zeta32.Arith.small_prime_crude_bound (r : ℚ) (n p : ℕ) : Nat.Prime p → ∀ (k : ℕ), (Qtilde r n).coeff k ≠ 0 → padicValRat p ((Qtilde r n).coeff k) ≥ -3 * (3 * ↑n) * ↑(Nat.log p (10 * n + 2)) - 3 * ↑n * ↑(padicValNat p r.den)