rh_right_half_certificate
plain-language theorem explainer
Under the RS Physical Thesis, the Riemann zeta function has no zeros with real part strictly greater than one half. Researchers connecting Recognition Science to analytic number theory cite this when establishing the right-half portion of the Riemann Hypothesis from the physical ledger. The proof is a one-line wrapper applying the implication derived from the thesis.
Claim. Assuming the RS Physical Thesis (every nontrivial zero of the Riemann zeta function in the open critical strip corresponds to a physical recognition event on the arithmetic ledger), for all complex numbers $s$, if the Riemann zeta function vanishes at $s$ and the real part of $s$ exceeds $1/2$, then the real part of $s$ equals $1/2$.
background
The Zeta-Ledger Bridge module connects Mathlib's riemannZeta to the DefectSensor and PhysicallyExists framework from UnifiedRH. The RS Physical Thesis asserts that every nontrivial zero of riemannZeta with real part in (1/2, 1) yields a zetaDefectSensor of charge one that satisfies PhysicallyExists. Upstream results include the LedgerFactorization structure for J-cost calibration and the PhiForcingDerived structure for the self-similar fixed point. The module documentation states that this thesis is the single non-mechanical ingredient needed to obtain the absence of strip zeros from the RS framework.
proof idea
This is a term proof consisting of a one-line wrapper that applies the right-half implication obtained from the RS Physical Thesis hypothesis.
why it matters
This declaration is used by the witnessed_physical_contradiction theorem to reach falsehood from any nonzero-charge physical sensor. It supplies the right-half direction in the Zeta-Ledger Bridge, realizing the module goal of deriving the Riemann Hypothesis from the RS thesis. The argument ties into the Recognition Science forcing chain through the J-uniqueness property and the phi-ladder defect analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.