RealizedCollapseBoundaryApproaching

formal source

 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
 336    simpa [mesh, hzero] using uniformChargeMesh_excess_zero N sensor.charge
 337  have hfloor_zero : annularTopologicalFloor N mesh.charge = 0 := by
 338    simpa [mesh, hzero] using (annularTopologicalFloor_zero N)
 339  have hcost_zero : annularCost mesh = 0 := by
 340    unfold annularExcess at hexcess_zero
 341    rw [hfloor_zero] at hexcess_zero
 342    linarith
 343  have hfalse : ¬ (1 < (0 : ℝ)) := by norm_num
 344  exact hfalse (by simpa [hcost_zero] using hcost)
 345
 346/-- Any cost-divergent sensor must have nonzero charge. -/
 347theorem costDivergent_charge_ne_zero (sensor : DefectSensor)
 348    (hdiv : CostDivergent sensor) :
 349    sensor.charge ≠ 0 := by
 350  intro hzero
 351  exact not_costDivergent_of_charge_zero sensor hzero hdiv
 352