theorem
proved
all_physicallyExist_of_rh
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Unification.UnifiedRH on GitHub at line 961.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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
965 exact (ontological_dichotomy sensor).mp (by
966 by_contra hm
967 exact hrh sensor hm)
968
969/-- **RH ↔ all sensors physically exist.** Machine-verified equivalence
970between the number-theoretic statement and the RS physical principle. -/
971theorem rh_iff_all_physical :
972 (∀ sensor : DefectSensor, sensor.charge ≠ 0 → False) ↔
973 (∀ sensor : DefectSensor, PhysicallyExists sensor) :=
974 ⟨all_physicallyExist_of_rh, rh_from_ontological_dichotomy⟩
975
976end UnifiedRH
977end Unification
978end IndisputableMonolith