Certified enclosure of the analytic constant C₀ for Zudilin’s parameters

Proved

ZudilinZeta.zudilin_numeric_C0_bounds

by tomasz · Oct 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysiscertified-numericsnumber-theoryzeta-values

For the parameters $r=3$ , $q=13$ , $\eta_0=91$ , $\eta_1=\eta_2=\eta_3=27$ , and $\eta_j=25+j$ for $4\le j\le13$ , let $\tau$ be any root of the characteristic polynomial in the upper half-plane whose real part is maximal among upper-half-plane roots. Then the analytic constant $C_0=-\operatorname{Re}f_0(\tau)$ satisfies

227.58019641\le C_0<227.58019642.

This is the analytic half of the numerical comparison in the proof of Zudilin’s theorem. The enclosure is uniform over every root satisfying the maximality condition, rather than an assumed decimal approximation to a chosen root.

Preamble

import Definitions.Def_ZudilinZetaAsymp
import Definitions.Def_ZudilinZetaParams13

Formal statement

namespace ZudilinZeta
theorem zudilin_numeric_C0_bounds (τ : ℂ) (hroot : charPoly params13 τ = 0) (him : 0 < τ.im)
    (hmax : ∀ σ : ℂ, charPoly params13 σ = 0 → 0 < σ.im → σ.re ≤ τ.re) :
    227.58019641 ≤ C0 params13 τ ∧ C0 params13 τ < 227.58019642 := by sorry
end ZudilinZeta

Source

W. Zudilin, Arithmetic of linear forms involving odd zeta values, https://arxiv.org/abs/math/0206176, Proposition 5 and proof of Theorem 3, printed pp. 34–35; the analytic constant is C0, and that paper denotes the mission arithmetic constant C1 by C2. Also One of the numbers ζ(5), ζ(7), ζ(9), ζ(11) is irrational, Russian Math. Surveys 56 (2001), 774–776.

View graph