theorem
proved
tactic proof
defect_budget_theorem
show as:
view Lean formalization →
formal statement (Lean)
229theorem defect_budget_theorem (L : DefectBoundedSubLedger)
230 (cls : CoarseGrainingStableClass L)
231 (h_all_flows : ∀ (cgf : CoarseGrainingFlow L), IsFlowStable L cgf cls) :
232 cls.z_charge = 0 := by
proof body
Tactic-mode proof.
233 -- Use the trivial flow with decreasing sequence converging to 0
234 let cgf : CoarseGrainingFlow L := {
235 coarsened_defect := fun n => L.defect / (n + 1 : ℝ)
236 at_zero := by simp
237 monotone_decrease := fun n => by
238 apply div_le_div_of_nonneg_left L.defect_nonneg
239 · positivity
240 · push_cast; linarith
241 nonneg := fun n => div_nonneg L.defect_nonneg (by positivity)
242 }
243 have hlimit : flowLimit cgf = 0 := by
244 unfold flowLimit cgf
245 simp only
246 apply le_antisymm _ (le_ciInf (fun n => div_nonneg L.defect_nonneg (by positivity)))
247 apply ciInf_le_of_le ⟨0, fun n => div_nonneg L.defect_nonneg (by positivity)⟩
248 intro ε hε
249 -- ∃ n such that L.defect / (n+1) < ε: take n = ceil(L.defect/ε)
250 use ⌈L.defect / ε⌉₊
251 apply div_lt_iff_lt_mul (by positivity) |>.mpr
252 calc L.defect < ε * (⌈L.defect / ε⌉₊ + 1 : ℝ) := by
253 have := Nat.lt_ceil.mpr (div_lt_div_of_lt_left L.defect_nonneg hε (le_refl ε))
254 nlinarith [this, hε]
255 exact flow_stable_at_zero L cgf cls (h_all_flows cgf) hlimit
256
257/-! ## Part 6: Status Summary -/
258
259/-- Status certificate for the RS Hodge formalization. -/