theorem
proved
tactic proof
j_cost_minimal_is_cgstable
show as:
view Lean formalization →
formal statement (Lean)
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
proof body
Tactic-mode proof.
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
109 · rw [h0]; exact L.defect_nonneg
110 · calc cyc.cycle_class.z_charge ≤ 1 := h1
111 _ ≤ L.defect + 1 := le_add_of_nonneg_left L.defect_nonneg
112 _ ≤ L.defect := by linarith [phi_pow44_gt_one L]
113 }
114 rfl
115 where
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. -/