proxyPhysicalizationBridge_of_charge_zero
plain-language theorem explainer
The theorem shows that any DefectSensor with zero charge satisfies the ProxyPhysicalizationBridge predicate. Researchers deriving the Riemann Hypothesis from the Recognition Science Euler-ledger construction cite this when restricting to charge-zero sensors. The proof is a one-line wrapper applying the reverse direction of the associated iff lemma.
Claim. Let $s$ be a defect sensor. If the charge of $s$ equals zero, then the ProxyPhysicalizationBridge holds for $s$: whenever there exists $K$ such that the defect of the scalar state at every $N$ is at most $K$, it follows that $s$ physically exists.
background
The module isolates the remaining transport step after a concrete directed Euler ledger, an admissible trace, and a T1-bounded realizability proxy have already been constructed for finite prime supports. ProxyPhysicalizationBridge(sensor) is the proposition that a uniform bound on the T1-defect of the realizability proxy implies PhysicallyExists(sensor). The defect functional equals the J-cost on positive reals, as defined in the Law of Existence.
proof idea
The proof is a one-line wrapper that applies the mpr direction of proxyPhysicalizationBridge_iff_charge_zero to the supplied hypothesis that the sensor charge is zero.
why it matters
This result closes the bridge for charge-zero sensors, the case needed for zeta-zero sensors. Once supplied, the module states that RSPhysicalThesis follows and therefore the Riemann Hypothesis. It sits downstream of the admissible Euler trace and realizability proxy constructions and upstream of the zero-induced bridge theorems in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.