flowLimit

formal source

 203  nonneg := fun _ => L.defect_nonneg
 204
 205/-- The limit of a coarse-graining flow is the asymptotic defect. -/
 206noncomputable def flowLimit (cgf : CoarseGrainingFlow L) : ℝ :=
 207  -- The infimum of a bounded-below decreasing sequence
 208  ⨅ n, cgf.coarsened_defect n
 209
 210/-- The flow limit is nonneg. -/
 211theorem flowLimit_nonneg (cgf : CoarseGrainingFlow L) : 0 ≤ flowLimit cgf :=
 212  le_ciInf (fun n => cgf.nonneg n)
 213
 214/-- A class is **coarse-graining stable** if its z_charge survives even the
 215    infinitely coarsened limit: z_charge ≤ flowLimit. -/
 216def IsFlowStable (L : DefectBoundedSubLedger) (cgf : CoarseGrainingFlow L)
 217    (cls : CoarseGrainingStableClass L) : Prop :=
 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