flow_stable_at_zero

formal source

 218  cls.z_charge ≤ flowLimit cgf
 219
 220/-- If a class is flow-stable and the flow converges to 0, the class has z_charge = 0. -/
 221theorem flow_stable_at_zero (L : DefectBoundedSubLedger) (cgf : CoarseGrainingFlow L)
 222    (cls : CoarseGrainingStableClass L) (hstable : IsFlowStable L cgf cls)
 223    (hlimit : flowLimit cgf = 0) : cls.z_charge = 0 := by
 224  have hle : cls.z_charge ≤ 0 := hlimit ▸ hstable
 225  exact le_antisymm hle cls.symmetric
 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