pith. machine review for the scientific record. sign in
def definition def or abbrev

ProxyPhysicalizationBridge

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  38def ProxyPhysicalizationBridge (sensor : DefectSensor) : Prop :=

proof body

Definition body.

  39  let pkg := concreteEulerLedgerOntologyInterface sensor
  40  letI : PhysicallyRealizableLedger sensor := pkg.realizableProxy
  41  (∃ K : ℝ, ∀ N : ℕ,
  42    IndisputableMonolith.Foundation.LawOfExistence.defect
  43      (PhysicallyRealizableLedger.scalarState (sensor := sensor) N) ≤ K) →
  44    PhysicallyExists sensor
  45
  46/-- If the proxy physicalization bridge holds for a sensor, then the concrete
  47Euler-ledger ontology package yields `PhysicallyExists` for that sensor. -/

used by (7)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (10)

Lean names referenced from this declaration's body.