513class CollapseBoundaryTransport (sensor : DefectSensor) 514 [PhysicallyRealizableLedger sensor] where 515 toLedgerBoundary : 516 ∀ (hm : sensor.charge ≠ 0), 517 RealizedCollapseBoundaryApproaching sensor hm → BoundaryApproaching sensor 518 519/-- Diagnostic one-scalar theorem: if one forcibly identifies the Euler ledger 520scalar with the realized collapse observable, transport to that scalar is 521immediate by definition. The impossibility theorem above shows why this 522identification cannot also satisfy the T1-bounded realizability interface. -/
used by (3)
From the project-wide theorem graph. These declarations reference this one in their body.