theorem
proved
tactic proof
realizedDefectCostBounded_iff_charge_zero_and_excessBounded
show as:
view Lean formalization →
formal statement (Lean)
294theorem realizedDefectCostBounded_iff_charge_zero_and_excessBounded
295 (fam : DefectSampledFamily) :
296 RealizedDefectAnnularCostBounded fam ↔
297 fam.sensor.charge = 0 ∧ RealizedDefectAnnularExcessBounded fam := by
proof body
Tactic-mode proof.
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. -/