defect_realizedDefectCollapseScalar

formal source

 399    exact lt_trans hlt_one hεgt
 400
 401/-- Closed form of the T1 defect on the realized collapse scalar. -/
 402theorem defect_realizedDefectCollapseScalar
 403    (sensor : DefectSensor) (hm : sensor.charge ≠ 0) (N : ℕ) :
 404    IndisputableMonolith.Foundation.LawOfExistence.defect
 405        (realizedDefectCollapseScalar sensor hm N) =
 406      annularCost ((canonicalDefectSampledFamily sensor hm).mesh N) ^ 2 /
 407        (2 * (1 + annularCost ((canonicalDefectSampledFamily sensor hm).mesh N))) := by
 408  let t : ℝ := annularCost ((canonicalDefectSampledFamily sensor hm).mesh N)
 409  have ht : 0 ≤ t := annularCost_nonneg _
 410  simpa [realizedDefectCollapseScalar, t] using defect_one_div_one_add t ht
 411
 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