eulerLedgerScalarState

formal source

 446/-- The actual Euler ledger scalar.  For charge `0` we stay at the stable value
 447`1`.  For nonzero charge we use the physically realized collapse observable
 448coming from the canonical defect family. -/
 449noncomputable def eulerLedgerScalarState (sensor : DefectSensor) (N : ℕ) : ℝ :=
 450  if hzero : sensor.charge = 0 then 1
 451  else realizedDefectCollapseScalar sensor hzero N
 452
 453/-- In the zero-charge sector, the Euler ledger scalar is identically `1`. -/
 454theorem eulerLedgerScalarState_eq_one (sensor : DefectSensor)
 455    (hzero : sensor.charge = 0) (N : ℕ) :
 456    eulerLedgerScalarState sensor N = 1 := by
 457  simp [eulerLedgerScalarState, hzero]
 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