proxyPhysicalizationBridge_of_charge_zero
plain-language theorem explainer
Sensors with zero charge satisfy the ProxyPhysicalizationBridge unconditionally. Workers closing the Recognition Science derivation of the Riemann hypothesis cite this result to connect bounded realizability proxies to physical existence. The proof applies the right-to-left direction of the charge-zero iff lemma in one step.
Claim. Let $s$ be a DefectSensor with charge zero. If there exists $K : ℝ$ such that for every $N : ℕ$ the defect of the scalar state of the realizability proxy at $N$ is at most $K$, then $s$ physically exists.
background
The Proxy Physicalization Bridge module isolates the transport from a bounded T1-defect realizability proxy (PhysicallyRealizableLedger) to the PhysicallyExists predicate after directed Euler ledgers are constructed. ProxyPhysicalizationBridge(sensor) is the statement that a uniform bound on defect(PhysicallyRealizableLedger.scalarState sensor N) for all N implies PhysicallyExists sensor, where defect is the J-cost functional from LawOfExistence. The module states that supplying this bridge for zeta-zero sensors yields RSPhysicalThesis and the Riemann hypothesis.
proof idea
The proof is a one-line wrapper that applies the right-to-left direction of proxyPhysicalizationBridge_iff_charge_zero to the hypothesis sensor.charge = 0.
why it matters
This theorem shows the ProxyPhysicalizationBridge holds for charge-zero sensors, which the module identifies as the zeta-zero sensors required for RSPhysicalThesis. It therefore supplies one direction of the remaining gap after the Euler-ledger and PhysicallyRealizableLedger constructions, feeding the siblings that derive zeroInducedBridge_iff_rsPhysicalThesis and rh_from_ZeroInducedProxyPhysicalizationBridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.