not_realizedDefectCollapseScalar_t1_bounded

formal source

 431/-- The current one-scalar closure target is impossible: the realized collapse
 432observable cannot have uniformly bounded T1 defect, because its defect is
 433already proved to be unbounded. -/
 434theorem not_realizedDefectCollapseScalar_t1_bounded
 435    (sensor : DefectSensor) (hm : sensor.charge ≠ 0) :
 436    ¬ ∃ K : ℝ, ∀ N : ℕ,
 437      IndisputableMonolith.Foundation.LawOfExistence.defect
 438        (realizedDefectCollapseScalar sensor hm N) ≤ K := by
 439  intro hbounded
 440  obtain ⟨K, hK⟩ := hbounded
 441  obtain ⟨N, hN⟩ := realizedDefectCollapseScalar_defect_unbounded sensor hm K
 442  exact not_lt_of_ge (hK N) hN
 443
 444/-! ## §6. Diagnostic one-scalar identification -/
 445
 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]