Small nonzero values of the forms (3) force an irrational among (4)

Proved

ZudilinZeta.zudilin_small_values_criterion

by Lucas · Sep 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysisirrationalitynumber-theoryzeta-values

The note states, between Lemmas 2 and 3: if the sequence of linear forms on the left-hand side of (3) takes nonzero arbitrarily small values as $n$ grows, then in the case $r = 3$ there is an irrational number among

\zeta(5),\ \zeta(7),\ \dots,\ \zeta(q-4),\ \zeta(q-2). \tag{4}

Formally: assume $r = 3$ and that for every $\varepsilon > 0$ there is an $n > 0$ with $\Lambda_n \ne 0$ and $|\Lambda_n| < \varepsilon$ , where $\Lambda_n = D^r_{m_1 n}D_{m_2 n}\cdots D_{m_{q-r}n}\Phi_n^{-1}F_n$ is the left-hand side of (3). Then at least one of $\zeta(r+2k)$ , $k = 1, \dots, (q-r-2)/2$ , is irrational.

This is the classical linear-form criterion applied to (3): by Lemma 1 the numbers $\Lambda_n$ lie in $\mathbb{Z} + \mathbb{Z}\zeta(5) + \dots + \mathbb{Z}\zeta(q-2)$ , and a nonzero integral linear combination of rationals cannot be arbitrarily small.

Preamble

import Definitions.Def_ZudilinZetaArith

Formal statement

namespace ZudilinZeta
theorem zudilin_small_values_criterion (P : Params) (hr : P.r = 3)
    (hsmall : ∀ ε : ℝ, 0 < ε → ∃ n : ℕ, 0 < n ∧ Lambda P n ≠ 0 ∧ |Lambda P n| < ε) :
    ∃ k ∈ Finset.Icc 1 ((P.q - P.r - 2) / 2), Irrational (zetaR (P.r + 2 * k)) := by sorry
end ZudilinZeta

Source

W. V. Zudilin, One of the numbers ζ(5), ζ(7), ζ(9), ζ(11) is irrational, Uspekhi Mat. Nauk 56:4 (2001), 149–150, https://doi.org/10.4213/rm427 (English transl.: Russian Math. Surveys 56:4 (2001), 774–776)

Read-back

What the Lean code literally says, in plain math · Aristotle by Harmonic (non-blind: same agent that drafted the statements)

Non-blind read-back — not independent testimony. This read-back was written by the same agent that drafted the Lean statement, at the human's explicit instruction, and not by an independent blind auditor. Its author had full knowledge of the intended meaning and of the source note, so it cannot corroborate the formalization the way a blind read-back would. A reviewer who wants genuine independent testimony should commission it separately.

The claim, for P : Params with P.r = 3: assume that for every real ε > 0 there is a natural number n with 0 < n, Lambda P n ≠ 0 and |Lambda P n| < ε. Then there exists k in Finset.Icc 1 ((P.q - P.r - 2) / 2) such that zetaR (P.r + 2 * k) is Irrational, i.e. not in the range of the cast ℚ → ℝ.

The index range uses natural-number subtraction and division, so it is 1, …, ⌊(q - r - 2)/2⌋. The hypothesis is exactly “arbitrarily small nonzero values”; it does not require the values to tend to zero, nor to be nonzero for all n.

Human review

Endorsed by Shuze Chen · Sep 24, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Sep 24, 2026
Confirmed by the mission captain (proposal self-audit).

View graph