ProxyPhysicalizationBridge
plain-language theorem explainer
ProxyPhysicalizationBridge encodes the sensor-level implication that a bounded T1-defect in the realizability proxy from the concrete Euler-ledger ontology yields PhysicallyExists for that DefectSensor. Number theorists deriving the Riemann Hypothesis from Recognition Science axioms cite this as the transport step closing the gap to RSPhysicalThesis. The definition directly packages the bounded-defect hypothesis into the existence conclusion using the ontology interface package.
Claim. Let $s$ be a defect sensor. The proxy physicalization bridge for $s$ holds when the following implication is true: if there exists a real $K$ such that the defect of the scalar state at every natural number $N$ under the physically realizable ledger for $s$ is at most $K$, then $s$ physically exists.
background
In the Proxy Physicalization Bridge module the concrete directed Euler ledger has already been built for every DefectSensor, producing an admissible Euler trace and a T1-bounded realizability proxy called PhysicallyRealizableLedger. The DefectSensor structure records the charge (multiplicity of the zeta zero) together with the real part of its location. The defect functional equals the J-cost for positive arguments and is supplied by LawOfExistence.defect. Upstream results include the EulerLedgerOntologyInterface, which furnishes the scalarDefectBounded property, and the Constants.K bridge ratio defined as phi to the power one-half.
proof idea
The definition obtains the concrete Euler ledger ontology package for the sensor, instantiates PhysicallyRealizableLedger from the package's realizableProxy field, and states the implication from the existence of a uniform bound K on scalar-state defects to the PhysicallyExists predicate.
why it matters
This definition supplies the missing transport for RSPhysicalThesis and hence RiemannHypothesis once the bridge is established for zeta-zero sensors. It is invoked directly in rh_from_ZeroInducedProxyPhysicalizationBridge and in the equivalence theorems proxyPhysicalizationBridge_iff_physicallyExists and proxyPhysicalizationBridge_iff_charge_zero. Within the Recognition framework it closes the final sensor-level gap after the T1-bounded proxy is in place, feeding the eight-tick octave and the derivation of D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.