A certified sufficient upper bound for Zudilin’s arithmetic constant

Proved

ZudilinZeta.zudilin_numeric_C1_upper_bound

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

analysiscertified-numericsnumber-theoryzeta-values

For Zudilin’s parameter tuple $(r,q)=(3,13)$ , $\eta_0=91$ , $\eta_1=\eta_2=\eta_3=27$ , and $\eta_j=25+j$ for $4\le j\le13$ , the arithmetic exponential-rate constant satisfies

C_1<\frac{455}{2}=227.5.

Together with the certified analytic bound $C_0\ge227.58019641$ , this supplies the strict inequality $C_1<C_0$ required by the irrationality criterion.

Preamble

import Definitions.Def_ZudilinZetaAsymp
import Definitions.Def_ZudilinZetaParams13

Formal statement

namespace ZudilinZeta
theorem zudilin_numeric_C1_upper_bound :
    C1 params13<227.5 := 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–36. This paper calls the mission arithmetic constant C2. The coarser upper bound here follows from certified finite truncation of the established periodic floor integral.

View graph