rh_from_rs_thesis
plain-language theorem explainer
The declaration shows that the Riemann Hypothesis follows once the RS Physical Thesis is assumed, identifying every nontrivial zeta zero in the critical strip as a physical recognition event. Researchers formalizing the Recognition Science derivation of RH would cite this as the final implication step. The proof works by case analysis on the real part of a hypothetical zero, applying the right-half result directly and mirroring via the completed zeta functional equation for the left half.
Claim. Assume the RS Physical Thesis: every nontrivial zero ρ of the Riemann zeta function with 1/2 < Re(ρ) < 1 corresponds to a physically existing defect sensor. Then the Riemann Hypothesis holds, i.e., every nontrivial zero has real part exactly 1/2.
background
The Zeta-Ledger Bridge module closes the gap between the DefectSensor/PhysicallyExists framework proved in UnifiedRH and Mathlib's concrete riemannZeta. RSPhysicalThesis is the single non-mechanical hypothesis: it asserts that every nontrivial zero ρ of riemannZeta in the open strip (1/2,1) yields a zetaDefectSensor whose charge is nonzero yet PhysicallyExists holds. Upstream results include the ontological dichotomy (charge = 0 ↔ PhysicallyExists), the right-half result rh_right_half_from_rs, and the functional equation for the completed zeta Λ(1-s) = Λ(s) with Γℝ nonzero at nontrivial zeros. The local setting is that all steps except this thesis are unconditional within the RS forcing chain.
proof idea
The proof intros a zero s with riemannZeta s = 0, nontriviality, and s ≠ 1. It cases on whether Re(s) > 1/2. The greater case applies rh_right_half_from_rs hrs s hzero hgt. Equality yields an immediate linarith contradiction. The less case invokes zeta_one_sub_zero_of_zero to produce a mirrored zero of 1-s in the right half-plane, applies rh_right_half_from_rs there, and derives the contradiction via the functional equation and linarith.
why it matters
This theorem is the direct parent of rh_certificate (RSPhysicalThesis → RiemannHypothesis) and is invoked by rh_from_ZeroInducedProxyPhysicalizationBridge and witnessed_physical_contradiction. It fills the final chain step from the RS thesis to Mathlib's RiemannHypothesis, relying on the T0-T8 forcing chain, the Recognition Composition Law, and the phi-ladder for the underlying ledger events. It touches the open question of deriving the RSPhysicalThesis itself from the zero-induced proxy or the full UnifiedRH framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.