nonzero_charge_not_physical
plain-language theorem explainer
A defect sensor with nonzero charge fails the physical existence predicate. Researchers formalizing the Riemann Hypothesis or deriving contradictions from strip zeros in Recognition Science cite this result. The proof is a one-line term application of the ontological dichotomy equivalence between zero charge and physical existence.
Claim. Let $s$ be a defect sensor. If the charge of $s$ is nonzero, then $s$ does not physically exist.
background
The Zeta-Ledger Bridge module connects the abstract DefectSensor framework proved in UnifiedRH to Mathlib's concrete riemannZeta function. A DefectSensor records the multiplicity (charge) of a zero of zeta, its real part, and confirms the location lies in the right half of the critical strip. The central upstream result is the ontological_dichotomy theorem, which states that a sensor physically exists if and only if its charge equals zero.
proof idea
The proof is a term-mode wrapper. It assumes physical existence of the sensor and applies the right-to-left direction of ontological_dichotomy to obtain that the charge must be zero, contradicting the nonzero-charge hypothesis.
why it matters
This result is invoked directly by unit_sensor_not_physical and witnessed_sensor_not_physical to show that concrete sensors built from strip zeros are non-physical. It supports the parent derivations of no_strip_zeros_from_rs and rh_from_rs_thesis in the same module. The declaration fills the unconditional step that any nonzero-charge sensor violates the RS physical thesis, without introducing custom axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.