rsPhysicalThesis_of_ZeroInducedProxyPhysicalizationBridge
plain-language theorem explainer
If every zeta zero in the critical strip satisfies the proxy physicalization bridge via its defect sensor, then the RS physical thesis holds. Researchers closing the Recognition Science derivation of the Riemann hypothesis cite this transport step. The proof is a one-line wrapper that feeds the zeta defect sensor and the bridge instance into the physicallyExists_of_ProxyPhysicalizationBridge lemma.
Claim. If for every complex number $ρ$ with $ζ(ρ)=0$ and $½ < Re(ρ) < 1$ the proxy physicalization bridge holds for the zeta defect sensor at real part $Re(ρ)$ with bounds $⟨½ < Re(ρ) < 1⟩$ and level 1, then the RS physical thesis holds.
background
The Proxy Physicalization Bridge module isolates the final transport after directed Euler ledgers and admissibility infrastructure are in place. For every DefectSensor one already has a concrete directed Euler ledger, an admissible trace, and a T1-bounded realizability proxy (PhysicallyRealizableLedger). The missing piece for RSPhysicalThesis is the step from that bounded proxy state to the PhysicallyExists predicate defined via eulerLedgerScalarState. ZeroInducedProxyPhysicalizationBridge packages the assumption that this transport succeeds exactly for the zeta-zero sensors constructed by zetaDefectSensor.
proof idea
One-line wrapper. It introduces the zero $ρ$ together with the strip bounds, builds the zeta defect sensor at real part $ρ.re$ with those bounds and level 1, then applies physicallyExists_of_ProxyPhysicalizationBridge directly to that sensor and the supplied bridge instance evaluated at $ρ$.
why it matters
This theorem supplies the missing link from the zero-induced bridge assumption to RSPhysicalThesis, which is immediately consumed by rh_from_ZeroInducedProxyPhysicalizationBridge to obtain the full RiemannHypothesis. The module doc-comment states that once the proxy physicalization bridge is proved for the zeta-zero sensors, both RSPhysicalThesis and RiemannHypothesis follow. It therefore closes the explicit gap left after the Euler ledger construction in the Recognition Science number-theory pipeline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.