no_strip_zeros_from_rs
plain-language theorem explainer
The RS physical thesis rules out zeros of the Riemann zeta function with real part strictly between one half and one. Researchers deriving the right-half form of the Riemann hypothesis from recognition science would cite this result. The proof is a direct one-line application of the unit-sensor-not-physical lemma to the defect sensor obtained by instantiating the thesis hypothesis.
Claim. If the RS physical thesis holds, then the Riemann zeta function has no zeros $ρ$ satisfying $1/2 < Re(ρ) < 1$.
background
The Zeta-Ledger Bridge module connects the abstract DefectSensor and PhysicallyExists framework (proved in UnifiedRH) to Mathlib's concrete riemannZeta function. The RS physical thesis asserts that every nontrivial zero of riemannZeta in the open critical strip corresponds to a physical ledger event, forcing the associated zetaDefectSensor to satisfy PhysicallyExists. The ontological dichotomy equates zero charge with physical existence and nonzero charge with non-existence. Upstream results include the zetaDefectSensor construction from strip data and the unit-sensor-not-physical lemma establishing the charge dichotomy.
proof idea
The proof is a one-line term that applies unit_sensor_not_physical to the real part of ρ together with the interval witnesses and the PhysicallyExists claim obtained by instantiating the RS physical thesis hypothesis at ρ.
why it matters
This result is invoked by rh_right_half_from_rs to conclude that every nontrivial zero with real part greater than one half must lie on the critical line. It supplies the inconsistency step between the RS physical thesis and any strip zero, as outlined in the module documentation. The argument uses only the thesis hypothesis plus the unconditionally proved ontological dichotomy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.