riemannZeta_ne_zero_re_ge_one
plain-language theorem explainer
The theorem asserts that the Riemann zeta function has no zeros for any complex s with real part at least 1. Analytic number theorists cite it as the classical de la Vallée-Poussin/Hadamard boundary result. The Lean proof is a one-line wrapper that invokes the corresponding Mathlib lemma on the half-plane.
Claim. For every complex number $s$ with $1 ≤ Re(s)$, the Riemann zeta function satisfies $ζ(s) ≠ 0$.
background
This declaration belongs to the StripZeroFreeRegion module, Phase 5 of the RS-native zeta program. The module records the proven Mathlib zero-free result on Re(s) ≥ 1 and distinguishes it from the still-needed logarithmic strip theorem for RH-quality closure. It imports the weak zero-free region and zeta-from-theta constructions to frame the boundary case as the unconditional starting point.
proof idea
The proof is a one-line wrapper that applies the Mathlib theorem riemannZeta_ne_zero_of_one_le_re directly to the real-part hypothesis.
why it matters
It supplies the ge_one field of boundaryZeroFreeCert and appears in the conjunction proved by phase5_current_state, which records the current unconditional region against the conditional strip bridge. The result anchors the classical Hadamard-de la Vallée-Poussin theorem inside the Recognition framework before any appeal to the phi-ladder or Recognition Composition Law. It leaves open the extension to the critical strip via StripZeroFreeBridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.