trivialFlow

formal source

 196  nonneg : ∀ n, 0 ≤ coarsened_defect n
 197
 198/-- Any DefectBoundedSubLedger admits a trivial (constant) coarse-graining flow. -/
 199def trivialFlow (L : DefectBoundedSubLedger) : CoarseGrainingFlow L where
 200  coarsened_defect := fun _ => L.defect
 201  at_zero := rfl
 202  monotone_decrease := fun _ => le_refl _
 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)