defect_budget_theorem

formal source

 226
 227/-- **Defect Budget Theorem**: A class that is stable under ALL coarse-graining flows
 228    (including those with limit 0) must have z_charge = 0. -/
 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
 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. -/