The numerical inequality (6.4): λ M₀ - I(ρ) + C* ≤ U

Only lower bounds for logarithms are needed. They come from the series log ((1+x)/(1-x)) = 2 ∑ x^(2k+1)/(2k+1), whose terms are nonnegative for 0 ≤ x < 1, so that partial sums are lower bounds, together with Mathlib's Real.log_two_lt_d9 for the range reduction log y = log (2^k y) - k log 2. The certificates (k, partial sums with 10 terms, rounded down) were generated by exact rational arithmetic; norm_num checks each one.

theorem Zeta5Irrational.log_ge_artanh {r : ℝ} (hr : 1 ≤ r) (m : ℕ) : 2 * ∑ k ∈ Finset.range m, 1 / (2 * ↑k + 1) * ((r - 1) / (r + 1)) ^ (2 * k + 1) ≤ Real.log r

Lower bound for log r, r ≥ 1, by a partial sum of the artanh series.

theorem Zeta5Irrational.log_ge_of_pow_two {y : ℝ} (hy : 0 < y) (k m : ℕ) (hk : 1 ≤ 2 ^ k * y) : 2 * ∑ j ∈ Finset.range m, 1 / (2 * ↑j + 1) * ((2 ^ k * y - 1) / (2 ^ k * y + 1)) ^ (2 * j + 1) - ↑k * 0.6931471808 ≤ Real.log y

Lower bound for log y, y > 0, after the range reduction by 2^k.

theorem Zeta5Irrational.energy_const : lam * M0 - Irho + Cstar ≤ ↑U

(6.4): λ M₀ - I(ρ) + C* ≤ U.