`realizedDefectCollapseScalar`

definition

show as: view math explainer →

module: IndisputableMonolith.Unification.UnifiedRH
domain: Unification
line: 305 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Unification.UnifiedRH on GitHub at line 305.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 302`collapse_N = 1 / (1 + annularCost(mesh_N))`.
 303
 304As the realized annular cost diverges, this scalar is forced toward `0`. -/
 305noncomputable def realizedDefectCollapseScalar
 306    (sensor : DefectSensor) (hm : sensor.charge ≠ 0) (N : ℕ) : ℝ :=
 307  1 / (1 + annularCost ((canonicalDefectSampledFamily sensor hm).mesh N))
 308
 309/-- The realized defect collapse scalar is always positive. -/
 310theorem realizedDefectCollapseScalar_pos
 311    (sensor : DefectSensor) (hm : sensor.charge ≠ 0) (N : ℕ) :
 312    0 < realizedDefectCollapseScalar sensor hm N := by
 313  unfold realizedDefectCollapseScalar
 314  apply one_div_pos.mpr
 315  have hcost_nonneg :
 316      0 ≤ annularCost ((canonicalDefectSampledFamily sensor hm).mesh N) :=
 317    annularCost_nonneg _
 318  linarith
 319
 320/-- Boundary-approach predicate for the concrete realized-defect collapse
 321scalar. -/
 322def RealizedCollapseBoundaryApproaching
 323    (sensor : DefectSensor) (hm : sensor.charge ≠ 0) : Prop :=
 324  ∀ ε > 0, ∃ N : ℕ, realizedDefectCollapseScalar sensor hm N < ε
 325
 326/-- Cost divergence is impossible for charge `0`. -/
 327theorem not_costDivergent_of_charge_zero (sensor : DefectSensor)
 328    (hzero : sensor.charge = 0) :
 329    ¬ CostDivergent sensor := by
 330  intro hdiv
 331  obtain ⟨N, hN⟩ := hdiv 1
 332  let mesh : AnnularMesh N := uniformChargeMesh N sensor.charge
 333  have hcost : 1 < annularCost mesh := by
 334    exact hN mesh (by intro n; rfl)
 335  have hexcess_zero : annularExcess mesh = 0 := by

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.