physical_sensor_charge_zero
plain-language theorem explainer
Every physically existing sensor carries zero topological charge. Researchers in recognition-based unification cite this as the direct corollary linking the Law of Existence to charge neutrality on the physical ledger. The proof is a one-line term that applies the right-to-left direction of the ontological dichotomy to the subtype membership predicate.
Claim. Let $ps$ be a sensor in the subtype of physically existing sensors (those with bounded T1 defect in the cost scalar). Then the topological charge of $ps$ equals zero.
background
The Unified RH module organizes T1-bounded realizability into cost divergence for nonzero charge, Euler trace admissibility for the carrier, and physically realizable ledgers. PhysicalSensor is the subtype of DefectSensor consisting of those sensors for which the PhysicallyExists predicate holds, i.e., the T1 defect of the associated scalar state remains uniformly bounded. The upstream ontological_dichotomy states that for any DefectSensor the charge equals zero if and only if there exists K such that the defect of the eulerLedgerScalarState is at most K for every natural number N; this is the RS ontological argument for RH.
proof idea
The proof is a term-mode one-liner. It invokes the right-to-left implication of the ontological_dichotomy theorem on the underlying sensor value and uses the subtype property to witness the bounded T1 defect.
why it matters
This supplies the charge-zero property invoked without hypotheses in the charge_zero_unconditional theorem of the RH_Certificate module. It realizes the core RS claim that the Law of Existence (T1) forces zero charge for every physically realizable sensor, since nonzero charge produces divergent annular cost forbidden by T1. The result closes the loop from the ontological dichotomy to physical existence and aligns with the forcing chain landmarks T1 and the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.