Generic criterion adapted from the Li₂ light-certificate project and the Apéry criterion in mo271/Zeta5 (Apache-2.0), with attribution retained.

theorem Zeta32.pow_mul_aeval_div_eq_intCast (p : Polynomial ℤ) {d : ℕ} (hd : p.natDegree ≤ d) (a b : ℤ) (hb : b ≠ 0) : ↑b ^ d * (Polynomial.aeval (↑a / ↑b)) p = ↑(∑ k ∈ Finset.range (d + 1), p.coeff k * a ^ k * b ^ (d - k))

theorem Zeta32.one_le_den_pow_mul_abs (Q : Polynomial ℤ) (q : ℚ) (d : ℕ) (hdeg : Q.natDegree ≤ d) (hne : (Polynomial.aeval ↑q) Q ≠ 0) : 1 ≤ ↑q.den ^ d * |(Polynomial.aeval ↑q) Q|

theorem Zeta32.irrational_of_int_polynomials (ξ : ℝ) (P : ℕ → Polynomial ℤ) (d : ℕ → ℕ) (hdeg : ∀ (n : ℕ), (P n).natDegree ≤ d n) (hdecay : ∀ (b : ℕ), 0 < b → Filter.Tendsto (fun (n : ℕ) => ↑b ^ d n * |(Polynomial.aeval ξ) (P n)|) Filter.atTop (nhds 0)) (hnonzero : ∀ (q : ℚ), ∃ᶠ (n : ℕ) in Filter.atTop, (Polynomial.aeval ↑q) (P n) ≠ 0) : Irrational ξ

theorem Zeta32.tendsto_pow_mul_exp_neg_sq_of_pos {c : ℝ} (hc : 0 < c) (D b : ℕ) (hb : 0 < b) : Filter.Tendsto (fun (n : ℕ) => ↑b ^ (D * n) * Real.exp (-c * ↑n ^ 2)) Filter.atTop (nhds 0)