Prove2Me

ζ\zeta has no zeros in the rectangle 0<Re⁡s<10<\operatorname{Re} s<1, ∣Im⁡s∣≤6|\operatorname{Im} s|\le 6

Proved
zeta_ne_zero_of_mem_strip_of_abs_im_le_six

by Gabewhigham · Sep 6, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

analytic-number-theorycomplex-analysisnumber-theoryzeta-functions

Let ζ\zeta denote the Riemann zeta function. The assertion is an unconditional, completely explicit zero-free region for the low-lying part of the critical strip, of height 66:

0<Re⁡s<1  and  ∣Im⁡s∣≤6 ⟹ ζ(s)≠0.0<\operatorname{Re} s<1 \ \text{ and } \ |\operatorname{Im} s|\le 6 \ \Longrightarrow\ \zeta(s)\neq 0.

The first nontrivial zero occurs at height ≈14.13\approx 14.13, so this is a proper truncation of the region in which zeros must be sought.

The proof is a quantitative estimate on the completed zeta function. Write Λ(s)=π−s/2Γ(s/2)ζ(s)\Lambda(s)=\pi^{-s/2}\Gamma(s/2)\zeta(s) and Λ0(s)=Λ(s)+1s+11−s\Lambda_0(s)=\Lambda(s)+\frac1s+\frac1{1-s} for its entire part, which is the Mellin transform

Λ0(s)=12∫0∞f(t) ts/2−1 dt\Lambda_0(s)=\tfrac12\int_0^\infty f(t)\,t^{s/2-1}\,dt

of the modified Jacobi theta kernel ff, with f(t)=θ(t)−1f(t)=\theta(t)-1 for t>1t>1 and f(t)=t−1/2(θ(1/t)−1)f(t)=t^{-1/2}(\theta(1/t)-1) for 0<t<10<t<1.

Comparison with a geometric series gives ∣θ(t)−1∣≤2110e−πt|\theta(t)-1|\le \tfrac{21}{10}e^{-\pi t} for t≥1t\ge1, so for 0<Re⁡s<10<\operatorname{Re} s<1 the Mellin integrand is dominated by 2110t−1/2e−πt\tfrac{21}{10}t^{-1/2}e^{-\pi t} on (1,∞)(1,\infty) and by 2110t−3/2e−π/t\tfrac{21}{10}t^{-3/2}e^{-\pi/t} on (0,1](0,1]; the substitution t↦1/tt\mapsto 1/t identifies the second integral with the first. Hence

∥Λ0(s)∥≤2110∫1∞u−1/2e−πu du≤0.0268,\|\Lambda_0(s)\|\le \frac{21}{10}\int_1^\infty u^{-1/2}e^{-\pi u}\,du\le 0.0268,

the tail integral being estimated by the elementary inequality u−1/2≤1−u−12+38(u−1)2u^{-1/2}\le 1-\tfrac{u-1}{2}+\tfrac38 (u-1)^2. On the other hand, in the rectangle 0<Re⁡s<10<\operatorname{Re} s<1, ∣Im⁡s∣≤6|\operatorname{Im} s|\le 6 one has ∥s∥ ∥1−s∥≤36⋅37<36.5\|s\|\,\|1-s\|\le\sqrt{36\cdot 37}<36.5, so

∥1s+11−s∥=1∥s∥ ∥1−s∥>136.5>0.0268.\left\|\frac1s+\frac1{1-s}\right\|=\frac1{\|s\|\,\|1-s\|}>\frac1{36.5}>0.0268 .

Therefore Λ(s)=Λ0(s)−1s−11−s\Lambda(s)=\Lambda_0(s)-\frac1s-\frac1{1-s} cannot vanish in the rectangle, and since π−s/2Γ(s/2)≠0\pi^{-s/2}\Gamma(s/2)\neq0 for Re⁡s>0\operatorname{Re} s>0, neither can ζ(s)\zeta(s).

Height 66 is close to the ceiling of this method: with the exact constants 2/(1−e−π)2/(1-e^{-\pi}) and ∫1∞u−1/2e−πudu=0.012178…\int_1^\infty u^{-1/2}e^{-\pi u}du=0.012178\ldots one gets ∥Λ0∥≤0.02547\|\Lambda_0\|\le 0.02547, which fails once ∥s∥∥1−s∥≥39.3\|s\|\|1-s\|\ge 39.3, i.e. above height ≈6.2\approx 6.2.

Formalization note. riemannZeta is Mathlib's zeta function; |s.im| is the absolute value of the imaginary part of ss.

Preamble
import Mathlib.NumberTheory.LSeries.RiemannZeta
import Mathlib.NumberTheory.LSeries.Nonvanishing

open Complex
Formal statement
theorem zeta_ne_zero_of_mem_strip_of_abs_im_le_six (s : ℂ) (h0 : 0 < s.re) (h1 : s.re < 1)
    (him : |s.im| ≤ 6) : riemannZeta s ≠ 0 := by sorry
Source
Standard theory of the completed Riemann zeta function; the quantitative form given here (bounding the entire part of the completed zeta function against its pole terms, with the substitution t -> 1/t on (0,1) and the tail bound for the incomplete Gamma integral) is elementary. See e.g. Titchmarsh, The Theory of the Riemann Zeta-Function, 2nd ed., Ch. II.

View graph