CollapseBoundaryTransport

formal source

 510approaches `0`, then the Euler ledger scalar approaches the T1 boundary as
 511well.  After redefining the ledger scalar to be the realized collapse
 512observable in the nonzero-charge sector, this becomes a theorem. -/
 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. -/
 523theorem euler_collapse_boundary_transport (sensor : DefectSensor)
 524    (hm : sensor.charge ≠ 0) :
 525    RealizedCollapseBoundaryApproaching sensor hm →
 526      ∀ ε > 0, ∃ N : ℕ, eulerLedgerScalarState sensor N < ε := by
 527  intro hcollapse ε hε
 528  obtain ⟨N, hN⟩ := hcollapse ε hε
 529  refine ⟨N, ?_⟩
 530  simpa [eulerLedgerScalarState, hm] using hN
 531
 532/-- Remaining ontology bridge after separating the bounded Euler realizability
 533proxy from the realized collapse observable: collapse of the realized defect
 534family must transport to boundary approach for the actual realizability proxy. -/
 535def EulerBoundaryBridgeAssumption : Prop :=
 536  ∀ sensor : DefectSensor,
 537    letI : PhysicallyRealizableLedger sensor := euler_physically_realizable sensor
 538    CollapseBoundaryTransport sensor
 539
 540/-- The old boundary-bridge interface is now recovered as a theorem: divergence
 541gives a concrete realized-defect collapse scalar that approaches `0`, and the
 542remaining proxy-transport hypothesis converts that collapse into boundary
 543approach for the bounded Euler realizability proxy. -/