Growth of the normaliser (Proposition 5.2, in the form needed here)

log m_K ≤ (A_eff + ε) K² for all large K, with A_eff = 1.36 < -U.

The bound assembles the four prime ranges:

• small primes p ≤ K/400: (6λ/400)K² by the prime number theorem;
• K/400 < p ≤ K/20: the tail bound, ≤ -0.05346 K²;
• K/20 < p ≤ K/3: the exact table, (5.18) K² = 0.04279 K²;
• K/3 < p ≤ 2h: the outer table, 129101/96000 K² = 1.34480 K²;

total ≈ 1.3480 K² + o(K²).

theorem Zeta5Irrational.low_order {δ : ℝ} (hδ : 0 < δ) : ∀ᶠ (n : ℕ) in Filter.atTop, 6 * (37 * ↑n) * ((√(200 * ↑n) + 1) * Real.log (200 * ↑n)) + 3 * 10 ^ 9 * ↑n ≤ δ * Kr n ^ 2

The lower-order terms are o(K²).

theorem Zeta5Irrational.theta_le_two (y : ℝ) (hy : 0 ≤ y) : Chebyshev.theta y ≤ 2 * y

theorem Zeta5Irrational.growth_mN (ε : ℝ) : 0 < ε → ∀ᶠ (n : ℕ) in Filter.atTop, Real.log ↑(mN n) ≤ (↑Aeff + ε) * Kr n ^ 2

Growth of the normaliser.