IsDefectBounded

formal source

  55  Finset.sum_nonneg (fun i _ => L.cost_nonneg i)
  56
  57/-- A sub-ledger is defect-bounded if its total defect is below a threshold. -/
  58def IsDefectBounded {n : ℕ} (L : SubLedger n) (bound : ℝ) : Prop :=
  59  totalDefect L ≤ bound
  60
  61/-! ## Cohomology Classes -/
  62
  63/-- A cohomology class on a sub-ledger. Abstract: represented by an
  64    integer (its "degree" in the discrete cohomology). -/
  65structure CohomologyClass where
  66  degree : ℤ
  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 →