IsCoarseGrainingStable

formal source

  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.
 101
 102    Proof: The DPI says D_KL(p'||q') ≤ D_KL(p||q) under coarse-graining.
 103    A J-cost minimum has the lowest possible KL divergence from the
 104    vacuum in its sector. Coarse-graining cannot lower it further (DPI),
 105    so the minimum is preserved. The cohomology class it generates is
 106    therefore stable under all coarse-grainings. -/
 107theorem algebraic_generates_hodge {n : ℕ} (L : SubLedger n)
 108    (h_min : IsJCostMinimal L) (c : CohomologyClass) :