zeta_ne_zero_re_ge_one
plain-language theorem explainer
The Riemann zeta function has no zeros with real part at least 1. This classical de la Vallée-Poussin region is invoked in the Recognition Science zeta-ledger bridge to close the right half-plane for derivations of the Riemann hypothesis. The proof is a direct one-line application of the corresponding Mathlib result.
Claim. For every complex number $s$ with $1 ≤ Re(s)$, the Riemann zeta function satisfies $ζ(s) ≠ 0$.
background
The Zeta–Ledger Bridge module connects the abstract DefectSensor and PhysicallyExists framework (proved in UnifiedRH) to Mathlib's concrete riemannZeta. It relies on the ontological dichotomy that a sensor charge equals zero if and only if the sensor physically exists, and introduces the RSPhysicalThesis hypothesis that every strip zero corresponds to a physical ledger event. This theorem supplies the classical zero-free region for Re(s) ≥ 1.
proof idea
The proof is a one-line wrapper that applies the Mathlib theorem establishing the de la Vallée-Poussin zero-free region to the hypothesis that the real part is at least one.
why it matters
This theorem supplies the classical zero-free region used in rh_right_half_from_rs to show that every nontrivial zero with real part greater than 1/2 must satisfy real part exactly 1/2 (vacuously, under the RS thesis). It fills the gap between the RS physical thesis and the full Riemann hypothesis by handling the right half-plane; the functional equation is still required for the left half. It touches the open question of deriving the complete Riemann hypothesis from the RS thesis alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.