Prove2Me

Zeros of ζ\zeta in the critical strip are symmetric under s↦1−ss\mapsto 1-s

Proved
zeta_zero_one_sub_of_mem_critical_strip

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

analytic-number-theorycomplex-analysisnumber-theoryriemann-zeta

Let ζ\zeta denote the Riemann zeta function. If ss lies in the open critical strip, 0<Re⁡s<10<\operatorname{Re} s<1, and ζ(s)=0\zeta(s)=0, then

ζ(1−s)=0.\zeta(1-s)=0.

In other words the zero set of ζ\zeta inside the critical strip is invariant under the reflection s↦1−ss\mapsto 1-s in the critical line Re⁡s=12\operatorname{Re} s=\tfrac12. This is an immediate consequence of Riemann's functional equation

ζ(1−s)=2(2π)−s Γ(s) cos⁡ ⁣(πs2)ζ(s),\zeta(1-s)=2(2\pi)^{-s}\,\Gamma(s)\,\cos\!\left(\frac{\pi s}{2}\right)\zeta(s),

whose hypotheses (ss not a nonpositive integer, s≠1s\neq1) are met throughout the strip.

The reflection symmetry is what allows a one-sided statement about the zeros — for instance that none of them has real part exceeding 12\tfrac12 — to be upgraded to the two-sided conclusion of the Riemann hypothesis.

Preamble
import Mathlib.NumberTheory.LSeries.RiemannZeta
import Mathlib.NumberTheory.LSeries.Nonvanishing
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
import Mathlib.Analysis.SpecialFunctions.Gamma.Beta

open Complex
Formal statement
theorem zeta_zero_one_sub_of_mem_critical_strip (s : ℂ) (h0 : 0 < s.re) (h1 : s.re < 1)
    (hz : riemannZeta s = 0) : riemannZeta (1 - s) = 0 := by sorry
Source
Riemann's functional equation and the resulting symmetry of the zeros in the critical strip: https://en.wikipedia.org/wiki/Riemann_zeta_function#Zeros,_the_critical_line,_and_the_Riemann_hypothesis. In Mathlib the functional equation used is `riemannZeta_one_sub`.

View graph