CoarseGrainingFlow

formal source

 185
 186/-- A coarse-graining flow on a sub-ledger: zooming out decreases the apparent defect.
 187    This is the RS analog of the heat flow in classical Hodge theory. -/
 188structure CoarseGrainingFlow (L : DefectBoundedSubLedger) where
 189  /-- Defect at scale 2^n (coarsened n times) -/
 190  coarsened_defect : ℕ → ℝ
 191  /-- At scale 0, we see the full defect -/
 192  at_zero : coarsened_defect 0 = L.defect
 193  /-- Coarse-graining is monotone: zooming out can only decrease apparent defect -/
 194  monotone_decrease : ∀ n, coarsened_defect (n + 1) ≤ coarsened_defect n
 195  /-- Defect is always nonneg -/
 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