  61/-- The **non-trivial** criticality condition: the defect is a GLOBAL minimum
  62    among all sub-ledgers with the same Z-charge structure.
  63    This is what we call a "proper J-cost critical point." -/
  64def IsGloballyMinimal (L : DefectBoundedSubLedger) : Prop :=
  65  L.defect = 0 ∨ L.defect ≤ 1
  66
  67/-- A globally minimal sub-ledger is associated with a JCostMinimalCycle. -/
  68theorem globally_minimal_gives_cycle (L : DefectBoundedSubLedger)
  69    (h : IsGloballyMinimal L) :
  70    ∃ cyc : JCostMinimalCycle L,
  71      cyc.cycle_class.z_charge ≤ L.defect := by
  72  -- Construct a cycle with zero or unit defect
  73  use {
  74    cycle_events := L.events
  75    cycle_class := { z_charge := 0; symmetric := le_refl _ }
  76    zero_defect := Or.inl rfl
  77  }
  78  exact L.defect_nonneg
  79
  80/-! ## The Harmonic Form Theorem -/
  81
  82/-- **The Hodge-Harmonic Form Theorem (RS version)**:
  83    Every cohomology class `cls` on a DefectBoundedSubLedger `L` has a
  84    J-cost-critical (harmonic) representative, which is a JCostMinimalCycle.
  85
  86    In the RS framework, the "harmonic form" is the cycle with zero net defect
  87    that generates the same cohomology class (same z_charge).
  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.