eulerLedgerScalarState_eq_collapse

formal source

 458
 459/-- In the nonzero-charge sector, the Euler ledger scalar is the concrete
 460realized collapse observable. -/
 461theorem eulerLedgerScalarState_eq_collapse (sensor : DefectSensor)
 462    (hm : sensor.charge ≠ 0) (N : ℕ) :
 463    eulerLedgerScalarState sensor N = realizedDefectCollapseScalar sensor hm N := by
 464  simp [eulerLedgerScalarState, hm]
 465
 466/-- The Euler ledger scalar is always positive. -/
 467theorem eulerLedgerScalarState_pos (sensor : DefectSensor) (N : ℕ) :
 468    0 < eulerLedgerScalarState sensor N := by
 469  by_cases hzero : sensor.charge = 0
 470  · simp [eulerLedgerScalarState, hzero]
 471  · simpa [eulerLedgerScalarState, hzero] using
 472      realizedDefectCollapseScalar_pos sensor hzero N
 473
 474/-- The Euler carrier is physically realizable in the T1-bounded sense with
 475realizability scalar given by the bounded carrier-derived proxy
 476`eulerScalarProxy`. -/
 477noncomputable instance eulerPhysicallyRealizableLedger (sensor : DefectSensor) :
 478    PhysicallyRealizableLedger sensor where
 479  admissible := euler_trace_admissible sensor
 480  scalarState := eulerScalarProxy sensor
 481  scalarStatePos := eulerScalarProxy_pos sensor
 482  scalarDefectBounded := eulerScalarProxy_defect_bounded sensor
 483
 484/-- Explicit theorem form of the Euler realizability instance. -/
 485noncomputable def euler_physically_realizable (sensor : DefectSensor) :
 486    PhysicallyRealizableLedger sensor := by
 487  infer_instance
 488
 489/-- The Euler proxy is itself a realizable scalar path, so it cannot approach
 490the T1 boundary. This makes explicit why a separate bridge theorem is needed:
 491its bounded carrier scale does not collapse on its own. -/