realizedDefectCostBounded_iff_charge_zero_and_excessBounded

formal source

 291realized-family refactor, the analytically natural target is no longer a bound
 292on arbitrary meshes, but a proof that the realized family has bounded excess
 293and hence can only occur with zero charge. -/
 294theorem realizedDefectCostBounded_iff_charge_zero_and_excessBounded
 295    (fam : DefectSampledFamily) :
 296    RealizedDefectAnnularCostBounded fam ↔
 297      fam.sensor.charge = 0 ∧ RealizedDefectAnnularExcessBounded fam := by
 298  constructor
 299  · intro hcost
 300    have hzero : fam.sensor.charge = 0 := by
 301      by_cases hm : fam.sensor.charge = 0
 302      · exact hm
 303      · obtain ⟨K, hK⟩ := hcost
 304        obtain ⟨N, hN⟩ := defect_cost_unbounded fam.sensor hm K
 305        have hcharge : ∀ n, ((fam.mesh N).rings n).winding = fam.sensor.charge := by
 306          intro n
 307          rw [((fam.mesh N).uniform_charge n), fam.charge_spec N]
 308        exact False.elim (not_lt_of_ge (hK N) (hN (fam.mesh N) hcharge))
 309    exact ⟨hzero, realizedDefectAnnularExcessBounded_of_costBounded fam hcost⟩
 310  · rintro ⟨hzero, hexcess⟩
 311    exact realizedDefectCostBounded_of_charge_zero_and_excessBounded fam hzero hexcess
 312
 313/-- **Quantitative target for the Axiom 2 attack.**
 314
 315The canonical realized defect family should have bounded excess above the
 316topological floor. This is the theorem that the current complex-analysis stack
 317ought to prove from local factorization `ζ⁻¹ = (z-ρ)^{-m} g(z)` together with a
 318log-derivative bound on the regular factor `g`.
 319
 320Once proved, `realizedDefectCostBounded_iff_charge_zero_and_excessBounded`
 321shows that Axiom 2 reduces exactly to forcing zero charge. -/
 322noncomputable def canonicalDefectSampledFamily_ringPerturbationControl
 323    (sensor : DefectSensor) (hm : sensor.charge ≠ 0) :
 324    RingPerturbationControl (canonicalDefectSampledFamily sensor hm) := by