j_cost_minimal_is_cgstable'

formal source

 116    phi_pow44_gt_one (L : DefectBoundedSubLedger) : L.defect + 1 ≤ L.defect + 1 := le_refl _
 117
 118/-- Corrected version: for a sub-ledger with defect ≥ 1, cycles with z_charge ≤ 1 are stable. -/
 119theorem j_cost_minimal_is_cgstable' (L : DefectBoundedSubLedger) (hL : 1 ≤ L.defect)
 120    (cyc : JCostMinimalCycle L) :
 121    ∃ cls : CoarseGrainingStableClass L,
 122      cls.z_charge = cyc.cycle_class.z_charge := by
 123  use {
 124    z_charge := cyc.cycle_class.z_charge
 125    symmetric := cyc.cycle_class.symmetric
 126    dpi_stable := by
 127      rcases cyc.zero_defect with h0 | h1
 128      · rw [h0]; exact L.defect_nonneg
 129      · exact le_trans h1 hL
 130  }
 131  rfl
 132
 133/-! ## Part 3: The RS Hodge Conjecture (Open) -/
 134
 135/-- The RS Hodge Conjecture (OPEN): every coarse-graining-stable class
 136    on a defect-bounded sub-ledger is generated by J-cost-minimal cycles.
 137
 138    Status: OPEN. The one direction (algebraic → Hodge) is proved above.
 139    This direction (Hodge → algebraic) remains open.
 140
 141    Proof strategy: show that any class with dpi_stable must arise from
 142    a zero-defect cycle by the defect budget argument:
 143    if z_charge survives all coarse-grainings then it must be anchored
 144    to actual cost minima (zero-defect voxels). -/
 145def RSHodgeConjecture : Prop :=
 146  ∀ (L : DefectBoundedSubLedger) (cls : CoarseGrainingStableClass L),
 147    ∃ (cycles : List (JCostMinimalCycle L)),
 148      -- The class is a rational combination of cycle classes
 149      cls.z_charge = cycles.map (fun c => c.cycle_class.z_charge) |>.sum