PhysicallyExists

formal source

 918
 919/-- A sensor physically exists iff its cost scalar has bounded T1 defect.
 920This is the RS existence criterion applied to the arithmetic ledger. -/
 921def PhysicallyExists (sensor : DefectSensor) : Prop :=
 922  ∃ K : ℝ, ∀ N : ℕ,
 923    IndisputableMonolith.Foundation.LawOfExistence.defect
 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,