The main estimate (Theorem 2.1 of the paper)

The three inputs of Section 7 of "ζ(5) is irrational" (A. Fauzan, 2026), all proved:

• degree_F: F_K has degree h = 37 n, (2.9) (Zeta5Irrational.Degree).
• real_bound: a weakening of Proposition 6.3, 0 < F_K(ζ(5)) and log F_K(ζ(5)) ≤ U K² + 27 K log K + 200 K (Zeta5Irrational.RealBound), using 27 in place of the paper's 24.
• normalization: positive rationals m_K with m_K F_K ∈ ℤ[X] (integral_mN) and log m_K ≤ (A_eff + ε) K² eventually (growth_mN), with A_eff = 1.36 < -U.

From these, main_estimate proves Theorem 2.1 with decay rate c = -800 (A_eff + U) > 0 in place of the paper's 139/5. This suffices for the irrationality criterion.

theorem Zeta5Irrational.degree_F (n : ℕ) : (F n).natDegree = 37 * n

(2.9): F_K has degree h = 37 n (proved in Zeta5Irrational.Degree).

theorem Zeta5Irrational.real_bound (n : ℕ) (hn : 0 < n) : 0 < (Polynomial.aeval zeta5) (F n) ∧ Real.log ((Polynomial.aeval zeta5) (F n)) ≤ ↑U * Kr n ^ 2 + 27 * Kr n * Real.log (Kr n) + 200 * Kr n

A weakening of Proposition 6.3, with 27 K log K in place of 24 K log K (see Zeta5Irrational.RealBound for its decomposition).

theorem Zeta5Irrational.normalization : ∃ (m : ℕ → ℚ), (∀ (n : ℕ), 0 < m n) ∧ (∀ᶠ (n : ℕ) in Filter.atTop, ∃ (Q : Polynomial ℤ), Polynomial.map (Int.castRingHom ℚ) Q = Polynomial.C (m n) * F n) ∧ ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in Filter.atTop, Real.log ↑(m n) ≤ (↑Aeff + ε) * Kr n ^ 2

Propositions 5.1 and 5.2 in the form proved here: a positive rational normalisation m_K with m_K F_K ∈ ℤ[X] for all n ≥ 1 (integral_mN), and for every ε > 0, eventually log m_K ≤ (A_eff + ε) K² (growth_mN).

theorem Zeta5Irrational.eventually_lower_order (δ : ℝ) (hδ : 0 < δ) : ∀ᶠ (n : ℕ) in Filter.atTop, 27 * Kr n * Real.log (Kr n) + 200 * Kr n < δ * Kr n ^ 2

The lower-order terms are eventually dominated: for every δ > 0, 27 K log K + 200 K < δ K² for all large n (with K = 40 n).

theorem Zeta5Irrational.main_estimate : ∃ (c : ℝ), 0 < c ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ∃ (Q : Polynomial ℤ), (∃ (c' : ℚ), 0 < c' ∧ Polynomial.map (Int.castRingHom ℚ) Q = Polynomial.C c' * F n) ∧ Q.natDegree = 37 * n ∧ 0 < (Polynomial.aeval zeta5) Q ∧ (Polynomial.aeval zeta5) Q < Real.exp (-c * ↑n ^ 2)

Theorem 2.1 of the paper, with the decay rate c = -800 (A_eff + U) > 0 instead of 139/5: for all large n, some positive rational multiple Q_n of F_{40n} is an integer polynomial of degree 37 n with 0 < Q_n(ζ(5)) < exp(-c n²).