zeta_one_sub_zero_of_zero
plain-language theorem explainer
zeta_one_sub_zero_of_zero shows that any nontrivial zero s of riemannZeta implies a zero at 1-s, provided s is not 1. It is invoked inside rh_from_rs_thesis to close the left half-plane case when deriving the Riemann hypothesis from the RS physical thesis. The proof is a short tactic sequence that transfers the zero via the completed zeta functional equation and recovers the ordinary zeta value from its meromorphic definition away from zero.
Claim. If $s$ is a nontrivial zero of the Riemann zeta function with $s$ not equal to 1, then $1-s$ is also a zero: if $s$ is not a negative even integer and $s$ is not 1, then $s$ is a nontrivial zero of $r$ implies $1-s$ is a nontrivial zero of $r$.
background
The Zeta-Ledger Bridge module connects the abstract DefectSensor and PhysicallyExists predicates (proved in UnifiedRH) to Mathlib's concrete riemannZeta. Nontrivial zeros are those outside the negative even integers; the completed zeta function satisfies the functional equation that swaps s and 1-s while preserving zeros. This lemma supplies the symmetry needed to map any left-half zero to a right-half zero. It depends on completedZeta_zero_of_nontrivial_zero (which lifts an ordinary zero to a completed zero) and on the definition of riemannZeta away from zero.
proof idea
The tactic proof first obtains 1-s ≠ 0 from the hypothesis s ≠ 1. It applies riemannZeta_def_of_ne_zero to express zeta(1-s) via completedRiemannZeta(1-s). It then rewrites completedRiemannZeta(1-s) to completedRiemannZeta(s) using completedRiemannZeta_one_sub and feeds the original zero into completedZeta_zero_of_nontrivial_zero. The final step divides by the nonzero gamma factor to conclude the ordinary zeta vanishes at 1-s.
why it matters
This lemma is used directly by rh_from_rs_thesis, the main result that derives Mathlib's RiemannHypothesis from the RS physical thesis. The module doc-comment notes that the left half-plane case follows from the completed zeta functional equation mapping left zeros to right zeros, after which the RS dichotomy plus de la Vallée-Poussin closes the argument. It fills the formalization gap between ledger events and the classical zeta function without introducing new axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.