rh_from_ZeroInducedProxyPhysicalizationBridge
plain-language theorem explainer
The theorem shows that the zero-induced proxy physicalization bridge for all non-trivial zeta zeros in the critical strip implies the Riemann hypothesis. Researchers connecting directed Euler ledgers to analytic number theory would cite this reduction step. The proof is a one-line wrapper composing the extraction of the RS physical thesis from the bridge with the known implication from that thesis to the hypothesis.
Claim. Let $B$ be the proposition that for every complex number $ρ$ with $ζ(ρ)=0$ and $1/2 < Re(ρ) < 1$, the proxy physicalization bridge holds for the corresponding zeta defect sensor. Then $B$ implies the Riemann hypothesis.
background
The module isolates the remaining transport gap after a directed Euler ledger over finite prime supports has been shown admissible and T1-bounded realizable. ZeroInducedProxyPhysicalizationBridge is defined as the universal statement that every strip zero of $ζ$ supplies a sensor for which the proxy-to-physical-existence bridge holds. The local setting records that the bounded-proxy hypothesis is already unconditional via EulerLedgerOntologyInterface.scalarDefectBounded, so the bridge reduces exactly to the PhysicallyExists predicate defined from eulerLedgerScalarState.
proof idea
One-line wrapper that applies rh_from_rs_thesis to the result of rsPhysicalThesis_of_ZeroInducedProxyPhysicalizationBridge instantiated on the supplied bridge argument.
why it matters
This supplies the forward direction of the equivalence ZeroInducedProxyPhysicalizationBridge ↔ RiemannHypothesis proved in zeroInducedBridge_iff_rh. It closes the reduction showing that the directed-ledger infrastructure isolates precisely the Riemann hypothesis as the remaining gap, expressed through T1-bounded realizability. The module documentation states that once the bridge is supplied for zeta-zero sensors, RSPhysicalThesis and hence the Riemann hypothesis follow.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.