nonzero_charge_impossible
plain-language theorem explainer
No defect sensor with nonzero charge can be physically realized. Researchers deriving the Riemann hypothesis from the Recognition Science forcing chain cite this as the direct contrapositive of the charge-existence dichotomy. The proof is a one-line term application of the prior lemma that nonzero charge precludes physical existence.
Claim. Let $S$ be a defect sensor. If the charge of $S$ is nonzero, then $S$ is not physically realizable.
background
In Recognition Science a defect sensor tracks ledger deviations with an associated charge that quantifies imbalance. The ontological dichotomy, proved in the unification layer, asserts that physical realizability holds precisely when charge vanishes. This theorem sits inside the RH Certificate module, which chains the law of existence (defect cost diverges as the argument approaches zero from above), annular coercivity, the dichotomy, and the zeta-ledger bridge to reach the full Riemann hypothesis statement.
proof idea
Term-mode proof consisting of a single application of the lemma that nonzero charge precludes physical existence, instantiated on the given sensor and the supplied inequality hypothesis.
why it matters
The result supplies the fourth step in the five-line RH certificate: any zeta zero inside the strip (1/2,1) would demand a unit-charge sensor that the dichotomy forbids. It therefore converts the RS physical thesis into the classical Riemann hypothesis. The argument rests only on the T0-T8 forcing chain, the recognition composition law, and the three standard Lean axioms; no additional hypotheses are introduced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.