rh_right_half_from_rs
plain-language theorem explainer
The theorem shows that the RS physical thesis implies no zeros of the Riemann zeta function exist with real part strictly between 1/2 and 1. An analytic number theorist deriving the Riemann hypothesis from ledger physics would cite this when connecting Recognition Science to classical zeta theory. The term proof proceeds by contradiction, case-splitting on whether the real part is less than 1 and applying the no-strip-zeros lemma or the classical non-vanishing result.
Claim. Let $ζ$ denote the Riemann zeta function. Assuming the RS physical thesis (every nontrivial zero in the open critical strip corresponds to a physical ledger event), then for all $s ∈ ℂ$, if $ζ(s) = 0$ and Re$(s) > 1/2$, it follows that Re$(s) = 1/2$.
background
The Zeta-Ledger Bridge module connects the DefectSensor and PhysicallyExists framework (proved in UnifiedRH) to Mathlib's riemannZeta. The hypothesis RSPhysicalThesis asserts that every nontrivial zero ρ of riemannZeta with 1/2 < Re(ρ) < 1 makes the associated zetaDefectSensor physically existent. The module documentation states that this thesis eliminates all zeros with 1/2 < Re(s) < 1. It builds on the ontological dichotomy (sensor charge zero iff physically exists) and upstream ledger factorization that defines J-cost and defect distances.
proof idea
The term proof introduces s with zeta(s) = 0 and Re(s) > 1/2, then derives a contradiction via exfalso. It cases on Re(s) < 1: the true branch applies no_strip_zeros_from_rs (using the RS thesis to contradict physical existence of a nonzero-charge sensor); the false branch applies zeta_ne_zero_re_ge_one (the classical result that zeta has no zeros for Re(s) ≥ 1).
why it matters
This supplies the right-half-plane half of the derivation of RiemannHypothesis from the RS thesis in the parent rh_from_rs_thesis. It closes the zeta-ledger bridge by showing the physical thesis is inconsistent with any zero having Re(s) > 1/2. In the Recognition Science framework it applies the ledger composition law and phi-forcing to arithmetic defects, realizing T5 J-uniqueness for the zeta function. The left-half direction follows from the functional equation in the downstream theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.