charge_zero_iff_physicallyExists

formal source

 924      (eulerLedgerScalarState sensor N) ≤ K
 925
 926/-- `ontological_dichotomy` restated: charge = 0 ↔ physically exists. -/
 927theorem charge_zero_iff_physicallyExists (sensor : DefectSensor) :
 928    sensor.charge = 0 ↔ PhysicallyExists sensor :=
 929  ontological_dichotomy sensor
 930
 931/-- The subtype of physically existing sensors — those whose cost scalar
 932has bounded T1 defect.  In RS, these are the sensors that correspond to
 933actual recognition events on the physical ledger. -/
 934def PhysicalSensor := { sensor : DefectSensor // PhysicallyExists sensor }
 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. -/
 947theorem physical_sensor_charge_zero (ps : PhysicalSensor) :
 948    ps.val.charge = 0 :=
 949  (ontological_dichotomy ps.val).mpr ps.property
 950
 951/-- **RH from the ontological dichotomy.**  If every sensor physically exists,
 952then every sensor has charge `0`. -/
 953theorem rh_from_ontological_dichotomy
 954    (h : ∀ sensor : DefectSensor, PhysicallyExists sensor) :
 955    ∀ (sensor : DefectSensor), sensor.charge ≠ 0 → False := by
 956  intro sensor hm
 957  exact hm ((ontological_dichotomy sensor).mpr (h sensor))