witnessed_sensor_not_physical
plain-language theorem explainer
Any witnessed defect sensor with nonzero charge maps to a DefectSensor that fails the PhysicallyExists predicate. Number theorists connecting Mathlib zeta zeros to the RS ledger would cite this to exclude physical strip zeros. The term-mode proof applies the core nonzero-charge non-existence result after a single charge projection rewrite.
Claim. Let $ws$ be a witnessed defect sensor (a structure carrying a point $rho$ in the open strip, integer charge, strip membership, and meromorphic order witness for $zetaReciprocal$ at $rho$) with charge nonzero. Then $ws$ does not physically exist: $¬$ PhysicallyExists$(ws.toDefectSensor)$.
background
The Zeta-Ledger Bridge module closes the gap between the abstract DefectSensor/PhysicallyExists framework proved in UnifiedRH and Mathlib's concrete riemannZeta. A WitnessedDefectSensor augments the basic sensor with an explicit complex point $rho$ in $(1/2,1)$, its integer charge, and the analytic witness meromorphicOrderAt zetaReciprocal rho = -charge. PhysicallyExists holds precisely when the associated eulerLedgerScalarState has T1 defect bounded by some $K$ for all natural numbers $N$. The upstream theorem nonzero_charge_not_physical asserts that any DefectSensor with nonzero charge fails PhysicallyExists, as a direct corollary of the ontological_dichotomy equivalence charge = 0 iff physically exists.
proof idea
The proof is a one-line wrapper that applies nonzero_charge_not_physical. The rwa tactic rewrites the charge hypothesis via the projection WitnessedDefectSensor.toDefectSensor_charge to match the lemma input exactly.
why it matters
This result is invoked directly by witnessed_physical_contradiction, which derives False from the assumption that a nonzero-charge witnessed sensor is physical. It advances the module program of showing that the RS physical thesis implies no strip zeros for zeta, hence derives the Riemann hypothesis. It supplies the witnessed-structure bridge between the unconditional ontological_dichotomy from UnifiedRH and the concrete zeta arguments needed for the RSPhysicalThesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.