not_proxyPhysicalizationBridge_of_charge_ne_zero
plain-language theorem explainer
Nonzero charge on a DefectSensor blocks the ProxyPhysicalizationBridge. Researchers linking zeta zeros to physical recognition events cite the result to exclude charged sensors from the physicalization step. The proof is a one-line wrapper that extracts PhysicallyExists from the bridge assumption and feeds it to the nonzero-charge obstruction.
Claim. Let $s$ be a DefectSensor with charge $c(s) ≠ 0$. Then the proxy physicalization bridge fails: it is not the case that a bounded T1 defect in the realizable proxy ledger implies PhysicallyExists($s$).
background
DefectSensor is the structure from CostCoveringBridge that records charge (multiplicity of a zeta zero) together with its real part. ProxyPhysicalizationBridge is the implication that bounded defect in the scalarState of a PhysicallyRealizableLedger supplied by the concrete Euler-ledger ontology package yields PhysicallyExists for the same sensor. The module isolates the final transport from bounded realizability proxies to actual physical existence after directed Euler ledgers and admissibility infrastructure are already in place, with the explicit goal of reaching RSPhysicalThesis and RiemannHypothesis once the bridge is granted for zero-charge sensors.
proof idea
The proof is a one-line wrapper. It assumes the bridge, applies physicallyExists_of_ProxyPhysicalizationBridge to obtain PhysicallyExists, then invokes nonzero_charge_not_physical on the nonzero charge hypothesis to reach a contradiction.
why it matters
The theorem is invoked inside zeroInducedBridge_iff_no_strip_zeros to equate ZeroInducedProxyPhysicalizationBridge with the absence of strip zeros. It supports the recognition science program by restricting physicalization to charge-zero sensors, thereby advancing the remaining gap to RSPhysicalThesis without constructing the bridge itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.