`proxyPhysicalizationBridge_iff_physicallyExists`

proved

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.ProxyPhysicalizationBridge
domain: NumberTheory
line: 93 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.NumberTheory.ProxyPhysicalizationBridge on GitHub at line 93.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  90/-- The proxy physicalization bridge is equivalent to physical existence.
  91The bounded-proxy hypothesis is unconditionally true, so the implication
  92reduces to its conclusion. -/
  93theorem proxyPhysicalizationBridge_iff_physicallyExists (sensor : DefectSensor) :
  94    ProxyPhysicalizationBridge sensor ↔ PhysicallyExists sensor := by
  95  constructor
  96  · exact physicallyExists_of_ProxyPhysicalizationBridge sensor
  97  · intro hphys
  98    let pkg := concreteEulerLedgerOntologyInterface sensor
  99    letI : PhysicallyRealizableLedger sensor := pkg.realizableProxy
 100    exact fun _ => hphys
 101
 102/-- The proxy physicalization bridge is equivalent to charge zero.
 103Combines the bridge-to-existence equivalence with the ontological
 104dichotomy `charge = 0 ↔ PhysicallyExists`. -/
 105theorem proxyPhysicalizationBridge_iff_charge_zero (sensor : DefectSensor) :
 106    ProxyPhysicalizationBridge sensor ↔ sensor.charge = 0 :=
 107  (proxyPhysicalizationBridge_iff_physicallyExists sensor).trans
 108    (charge_zero_iff_physicallyExists sensor).symm
 109
 110/-- The bridge holds unconditionally for charge-zero sensors. -/
 111theorem proxyPhysicalizationBridge_of_charge_zero (sensor : DefectSensor)
 112    (h : sensor.charge = 0) : ProxyPhysicalizationBridge sensor :=
 113  (proxyPhysicalizationBridge_iff_charge_zero sensor).mpr h
 114
 115/-- The bridge fails for any sensor with nonzero charge: the cost scalar
 116collapses and T1 defect diverges, so `PhysicallyExists` is false. -/
 117theorem not_proxyPhysicalizationBridge_of_charge_ne_zero (sensor : DefectSensor)
 118    (hm : sensor.charge ≠ 0) : ¬ ProxyPhysicalizationBridge sensor := by
 119  intro hbridge
 120  exact nonzero_charge_not_physical sensor hm
 121    (physicallyExists_of_ProxyPhysicalizationBridge sensor hbridge)
 122
 123/-- `ZeroInducedProxyPhysicalizationBridge` is logically equivalent to

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.