harmonic_form_theorem_zero_charge

formal source

  88
  89    STATUS: THEOREM for the case cls.z_charge = 0;
  90            HYPOTHESIS for the general case (requires the full defect budget argument). -/
  91theorem harmonic_form_theorem_zero_charge (L : DefectBoundedSubLedger)
  92    (cls : CoarseGrainingStableClass L)
  93    (h_zero : cls.z_charge = 0) :
  94    ∃ cyc : JCostMinimalCycle L, cyc.cycle_class.z_charge = cls.z_charge := by
  95  use {
  96    cycle_events := L.events
  97    cycle_class := { z_charge := 0; symmetric := le_refl _ }
  98    zero_defect := Or.inl rfl
  99  }
 100  exact h_zero.symm
 101
 102/-- **Harmonic Form Theorem for Globally Minimal Sub-Ledgers**:
 103    When the sub-ledger has defect ≤ 1, every stable class has z_charge ≤ 1
 104    and hence is generated by a JCostMinimalCycle. -/
 105theorem harmonic_form_theorem_minimal_ledger (L : DefectBoundedSubLedger)
 106    (h_min : L.defect ≤ 1)
 107    (cls : CoarseGrainingStableClass L) :
 108    ∃ cyc : JCostMinimalCycle L, cyc.cycle_class.z_charge = cls.z_charge := by
 109  -- cls.z_charge ≤ L.defect ≤ 1, so the cycle with zero_defect holds via ≤ 1 case
 110  use {
 111    cycle_events := L.events
 112    cycle_class := { z_charge := cls.z_charge; symmetric := cls.symmetric }
 113    zero_defect := Or.inr cls.dpi_stable
 114  }
 115
 116/-! ## Critical Points and the Hodge Decomposition -/
 117
 118/-- The Hodge decomposition: every cohomology class decomposes as
 119    (harmonic part) + (exact part) + (coexact part).
 120    In RS: every stable class = (zero-defect cycle) + (boundary correction). -/
 121structure HodgeDecomposition (L : DefectBoundedSubLedger) (cls : CoarseGrainingStableClass L) where