Section 6 of the paper: the real determinant, decomposed

A variant of Proposition 6.3 (real_bound) with 27 K log K in place of the paper's 24 K log K is derived from

• Δ_pos : Δ_K(ζ(5)) > 0 — proved in Zeta5Irrational.Positivity from the moment representation moment_rep (Proposition 2.2);
• log_Δ_le: a variant of (6.14) with 22 h log K + 50 h in place of 18 h log K + 160 h, proved in Zeta5Irrational.EnergyBound from Andréief's identity (6.10), variants of (6.11)–(6.12), and the variant of (6.9) energy_ineq (proved in Zeta5Irrational.EnergyFinal from Lemmas 6.1 and 6.2);
• energy_const : the numerical inequality (6.4), λ M₀ - I(ρ) + C* ≤ U — Appendix A.4 — proved in Zeta5Irrational.EnergyConst;
• log_S_le : the Stirling bound (6.15) — proved.

theorem Zeta5Irrational.log_Δ_le (n : ℕ) (hn : 0 < n) : Real.log ((Polynomial.aeval zeta5) (Δ n)) ≤ 2 * (37 * ↑n) * (37 * ↑n + 6 * (3 * ↑n) - 40 * ↑n) * Real.log (Kr n) + (lam * M0 - Irho) * Kr n ^ 2 + 22 * (37 * ↑n) * Real.log (Kr n) + 50 * (37 * ↑n)

A variant of (6.14) with 22 h log K + 50 h instead of 18 h log K + 160 h, proved in Zeta5Irrational.EnergyBound from the configuration inequality energy_ineq.

theorem Zeta5Irrational.log_S_le (n : ℕ) (hn : 0 < n) : Real.log ↑(S n) ≤ (2 * lam - 12 * alph * lam - 2 * lam ^ 2) * Kr n ^ 2 * Real.log (Kr n) + Cstar * Kr n ^ 2 + 6 * (37 * ↑n) * Real.log (Kr n) + 6 * (37 * ↑n)

(6.15): the Stirling bound for log S_K.

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, from the four statements above: we use 27 K log K in place of the paper's 24 K log K.