PhysicalSensor

formal source

 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))
 958
 959/-- The converse: RH implies all sensors physically exist (vacuously —
 960charge `0` sensors are T1-bounded). -/
 961theorem all_physicallyExist_of_rh
 962    (hrh : ∀ sensor : DefectSensor, sensor.charge ≠ 0 → False) :
 963    ∀ sensor : DefectSensor, PhysicallyExists sensor := by
 964  intro sensor