pith. machine review for the scientific record. sign in
theorem proved term proof

defect_realizedDefectCollapseScalar

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 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

proof body

Term-mode proof.

 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. -/

depends on (12)

Lean names referenced from this declaration's body.