realizedDefectCollapseScalar_defect_unbounded

formal source

 412/-- Because the realized collapse scalar approaches `0`, its T1 defect is itself
 413unbounded above.  This is the exact obstruction to making that scalar the
 414uniformly realizable Euler ledger proxy. -/
 415theorem realizedDefectCollapseScalar_defect_unbounded
 416    (sensor : DefectSensor) (hm : sensor.charge ≠ 0) :
 417    ∀ C : ℝ, ∃ N : ℕ,
 418      C <
 419        IndisputableMonolith.Foundation.LawOfExistence.defect
 420          (realizedDefectCollapseScalar sensor hm N) := by
 421  intro C
 422  obtain ⟨ε, hεpos, hε⟩ := t1_cost_barrier C
 423  obtain ⟨N, hN⟩ :=
 424    realizedDefectCollapseBoundaryApproaching_of_nonzero_charge sensor hm ε hεpos
 425  refine ⟨N, ?_⟩
 426  exact hε
 427    (realizedDefectCollapseScalar sensor hm N)
 428    (realizedDefectCollapseScalar_pos sensor hm N)
 429    hN
 430
 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