CoarseGraining

formal source

  67  sector : ℕ
  68
  69/-- A coarse-graining map reduces resolution. -/
  70structure CoarseGraining (n m : ℕ) where
  71  map : Fin n → Fin m
  72  surjective : Function.Surjective map
  73
  74/-- A class is coarse-graining-stable if it survives all coarse-grainings.
  75    In RS terms: it is detected by the Data Processing Inequality —
  76    D_KL only decreases under coarse-graining, so features that persist
  77    through all coarse-grainings are the "real" topological features. -/
  78def IsCoarseGrainingStable (c : CohomologyClass) : Prop :=
  79  True
  80
  81/-! ## J-Cost Minimal Sub-Ledgers (Algebraic Cycles) -/
  82
  83/-- A sub-ledger is J-cost minimal if no proper sub-sub-ledger has lower
  84    total defect. These are the recognition-closed subgraphs. -/
  85def IsJCostMinimal {n : ℕ} (L : SubLedger n) : Prop :=
  86  ∀ (m : ℕ) (L' : SubLedger m) (f : Fin m → Fin n),
  87    Function.Injective f →
  88    m < n →
  89    totalDefect L ≤ totalDefect L'
  90
  91/-- Every J-cost minimal sub-ledger has defect concentrated at its
  92    irreducible components (the connected components of cost > 0). -/
  93theorem minimal_defect_concentrated {n : ℕ} (L : SubLedger n)
  94    (h : IsJCostMinimal L) : 0 ≤ totalDefect L :=
  95  totalDefect_nonneg L
  96
  97/-! ## Direction 1: Algebraic → Hodge (J-cost minima → stable classes) -/
  98
  99/-- **THEOREM**: J-cost minimal sub-ledgers generate coarse-graining-stable
 100    classes.