zeroInducedBridge_of_rh
plain-language theorem explainer
Mathlib's RiemannHypothesis implies ZeroInducedProxyPhysicalizationBridge, the statement that every zeta zero in the open critical strip satisfies the proxy physicalization bridge for its defect sensor. Researchers reducing the Recognition Science physical thesis to the Riemann hypothesis cite this direction. The proof rewrites the bridge to its no-strip-zeros form, rules out trivial zeros and the pole at 1, then applies the hypothesis to reach a contradiction via linear arithmetic.
Claim. If the Riemann hypothesis holds, then for every complex number $ρ$ with $ζ(ρ)=0$ and $1/2 < Re(ρ) < 1$, the proxy physicalization bridge holds for the zeta defect sensor at $Re(ρ)$.
background
ZeroInducedProxyPhysicalizationBridge is the universal statement that every non-trivial zeta zero in the open strip (1/2 < Re(ρ) < 1) induces a zetaDefectSensor for which ProxyPhysicalizationBridge holds. The module isolates the remaining transport from PhysicallyRealizableLedger (already constructed via directed Euler ledgers over finite primes) to the actual PhysicallyExists predicate defined by eulerLedgerScalarState. This completes the reduction path from the admissible Euler trace to RSPhysicalThesis once the bridge is supplied for zeta-zero sensors.
proof idea
The tactic proof rewrites via zeroInducedBridge_iff_no_strip_zeros, then intros ρ, hzero, hlo, hhi. It derives a contradiction for trivial zeros by equating real parts and applying linarith on non-negative integers. It rules out ρ = 1 by substituting into hhi and using linarith. The final linarith step invokes the supplied RiemannHypothesis hypothesis directly on the remaining strip zero.
why it matters
This supplies the backward direction of zeroInducedBridge_iff_rh, establishing exact equivalence between ZeroInducedProxyPhysicalizationBridge and RiemannHypothesis. The equivalence closes the reduction in the Proxy Physicalization Bridge module: the directed-ledger infrastructure isolates a gap that is precisely the Riemann hypothesis, with no remainder. It thereby links the number-theoretic sensor construction to the RS physical thesis without additional hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.