An irrationality criterion via integer polynomials

This file proves the elementary reduction used in the paper "ζ(5) is irrational" (A. Fauzan, 17 September 2026), Section 1.1 / proof of Theorem 1.1:

If ξ is a real number and for all sufficiently large n there is an integer polynomial Q of degree at most d n with 0 < Q(ξ) ≤ ε n, where b ^ (d n) * ε n → 0 for every positive integer b, then ξ is irrational.

The point is that if ξ = a / b then b ^ (d n) * Q(a / b) is a positive integer, hence at least 1, while it tends to zero.

theorem Zeta5Irrational.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))

Clearing denominators: for p : ℤ[X] of degree at most d, the number b ^ d * p(a / b) is the integer ∑ k, coeff k * a ^ k * b ^ (d - k).

theorem Zeta5Irrational.irrational_of_eventually_exists_int_poly (ξ : ℝ) (d : ℕ → ℕ) (ε : ℕ → ℝ) (hε : ∀ (b : ℕ), 0 < b → Filter.Tendsto (fun (n : ℕ) => ↑b ^ d n * ε n) Filter.atTop (nhds 0)) (h : ∀ᶠ (n : ℕ) in Filter.atTop, ∃ (Q : Polynomial ℤ), Q.natDegree ≤ d n ∧ 0 < (Polynomial.aeval ξ) Q ∧ (Polynomial.aeval ξ) Q ≤ ε n) : Irrational ξ

Irrationality criterion. Let ξ : ℝ, d : ℕ → ℕ and ε : ℕ → ℝ be such that b ^ (d n) * ε n → 0 for every positive integer b. If for all sufficiently large n there is an integer polynomial Q with natDegree Q ≤ d n and 0 < Q(ξ) ≤ ε n, then ξ is irrational.

theorem Zeta5Irrational.tendsto_pow_mul_exp_neg_sq_of_pos_degree {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)

Gaussian decay dominates every fixed linear power exponent.

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

The decay b ^ (37 n) * exp (-c n²) → 0 for every c > 0.

theorem Zeta5Irrational.tendsto_pow_mul_exp_neg_sq (b : ℕ) (hb : 0 < b) : Filter.Tendsto (fun (n : ℕ) => ↑b ^ (37 * n) * Real.exp (-(139 / 5) * ↑n ^ 2)) Filter.atTop (nhds 0)

The specific decay used in the paper: b ^ (37 n) * exp (-(139/5) n²) → 0.