pith. machine review for the scientific record. sign in
theorem proved tactic proof

j_cost_minimal_is_cgstable'

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 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

proof body

Tactic-mode proof.

 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). -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (27)

Lean names referenced from this declaration's body.