proxyPhysicalizationBridge_iff_charge_zero
plain-language theorem explainer
The theorem states that for any defect sensor the proxy physicalization bridge holds exactly when the sensor charge is zero. Researchers reducing the Riemann hypothesis inside the Recognition Science ledger framework would cite this link between the bridge predicate and the ontological dichotomy. The proof is a one-line term composition that chains two prior equivalences via transitivity and symmetry.
Claim. Let $s$ be a defect sensor. The proxy physicalization bridge holds for $s$ if and only if the charge of $s$ is zero, where the bridge asserts that bounded T1 defect of the realizability proxy implies physical existence for $s$.
background
The Proxy Physicalization Bridge module isolates the final transport step after the directed Euler ledger supplies a PhysicallyRealizableLedger. A DefectSensor records the multiplicity (its charge) and real part of a zeta zero. ProxyPhysicalizationBridge for a sensor requires that bounded T1 defect of the scalar state implies PhysicallyExists for that sensor. Upstream, proxyPhysicalizationBridge_iff_physicallyExists proves the bridge is equivalent to PhysicallyExists because the boundedness hypothesis holds unconditionally. charge_zero_iff_physicallyExists from UnifiedRH restates the ontological dichotomy as charge zero if and only if PhysicallyExists.
proof idea
The proof is a term-mode one-liner. It applies transitivity to the equivalence proxyPhysicalizationBridge_iff_physicallyExists sensor and the symmetric form of charge_zero_iff_physicallyExists sensor.
why it matters
This equivalence supports proxyPhysicalizationBridge_of_charge_zero and is used in zeroInducedBridge_iff_rh, which equates the zero-induced bridge directly to the Riemann hypothesis. It completes one link in the reduction from the concrete Euler-ledger infrastructure to RH, consistent with the T5 J-uniqueness and T8 dimension forcing steps of the broader framework. The result is fully proved with no remaining scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.