935 936/-- **RS Ontological Theorem**: every physically existing sensor has 937charge `0`. 938 939This is the core RS result. It is: 940* Unconditional — no hypotheses beyond the subtype constraint 941* Axiom-free — depends only on `propext`, `Classical.choice`, `Quot.sound` 942* A direct corollary of `ontological_dichotomy` 943 944In RS language: the Law of Existence (T1) forces every physical recognition 945event to have zero topological charge. Nonzero charge requires divergent 946cost, which T1 forbids for physically realizable ledger entries. -/
used by (4)
From the project-wide theorem graph. These declarations reference this one in their body.