proxyPhysicalizationBridge_iff_physicallyExists
plain-language theorem explainer
The equivalence shows that the proxy physicalization bridge for a defect sensor holds if and only if the sensor satisfies physical existence. Researchers reducing the Riemann hypothesis inside Recognition Science would cite this to link the T1-bounded realizability proxy to the PhysicallyExists predicate. The term-mode proof applies an upstream implication lemma in one direction and constructs the concrete Euler-ledger ontology package to discharge the implication in the other.
Claim. Let $σ$ be a defect sensor. The proxy physicalization bridge for $σ$ holds if and only if $σ$ physically exists.
background
This declaration appears in the Proxy Physicalization Bridge module, which isolates the remaining gap after the concrete directed Euler-ledger system has been built and connected to the admissibility and realizability infrastructure. For every defect sensor one now possesses a concrete directed Euler ledger over finite prime supports, an admissible Euler trace, and a T1-bounded realizability proxy supplied by PhysicallyRealizableLedger.
proof idea
The proof is a term-mode constructor establishing the biconditional. The forward direction applies the upstream lemma physicallyExists_of_ProxyPhysicalizationBridge. The reverse direction introduces the physical-existence hypothesis, builds the concrete Euler ledger ontology interface package for the sensor, instantiates the PhysicallyRealizableLedger, and returns a constant function that ignores any bounded-defect premise.
why it matters
This equivalence lets the proxy physicalization bridge be identified with physical existence and therefore combines with the charge-zero dichotomy to produce the further equivalence to charge zero. It is used directly by the theorems that equate the zero-induced proxy physicalization bridge with both the RS physical thesis and the Riemann hypothesis. In the Recognition Science framework it closes the transport from the bounded proxy state to the PhysicallyExists predicate, reducing the remaining gap for RSPhysicalThesis precisely to the Riemann hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.