CoarseGrainingStableClass

formal source

  75    "zooming out" — the Data Processing Inequality (DPI).
  76    A class survives coarse-graining iff its z_charge is anchored to
  77    the actual J-cost structure (not just a statistical artifact). -/
  78structure CoarseGrainingStableClass (L : DefectBoundedSubLedger) extends CohomologyClass L where
  79  /-- Stability condition: z_charge is a fixed point under DPI -/
  80  dpi_stable : z_charge ≤ L.defect
  81
  82/-- A JCostMinimalCycle is a recognition-closed subgraph with zero net defect:
  83    the RS analog of an algebraic cycle. Every boundary node is balanced. -/
  84structure JCostMinimalCycle (L : DefectBoundedSubLedger) where
  85  /-- The events in the cycle -/
  86  cycle_events : List RecognitionEvent
  87  /-- The cycle generates a cohomology class (its topological charge) -/
  88  cycle_class : CohomologyClass L
  89  /-- Zero-defect condition: the cycle's J-cost sums to zero
  90      (every debit is matched by a credit — double-entry structure) -/
  91  zero_defect : cycle_class.z_charge = 0 ∨
  92    -- Or: z_charge ≤ 1 (near-zero, within one recognition tick)
  93    cycle_class.z_charge ≤ 1
  94
  95/-! ## Part 2: One Direction — Algebraic ⟹ Hodge -/
  96
  97/-- Every JCostMinimalCycle is a CoarseGrainingStableClass.
  98    This is the easy direction: cost minima always survive coarse-graining,
  99    because zooming out can only reduce (not increase) the defect budget. -/
 100theorem j_cost_minimal_is_cgstable (L : DefectBoundedSubLedger)
 101    (cyc : JCostMinimalCycle L) :
 102    ∃ cls : CoarseGrainingStableClass L,
 103      cls.z_charge = cyc.cycle_class.z_charge := by
 104  use {
 105    z_charge := cyc.cycle_class.z_charge
 106    symmetric := cyc.cycle_class.symmetric
 107    dpi_stable := by
 108      rcases cyc.zero_defect with h0 | h1