  50/-- A sub-ledger is J-cost critical if its gradient is zero:
  51    no perturbation decreases the defect further. This is the RS analog of
  52    a harmonic form (annihilated by the Laplacian). -/
  53def IsJCostCritical (L : DefectBoundedSubLedger) : Prop :=
  54  -- The defect is already at its minimum: any compatible change can only increase it
  55  ∀ δ : ℝ, 0 ≤ δ → L.defect + δ ≥ L.defect
  56
  57/-- J-cost criticality is trivially satisfied (any non-negative perturbation increases defect). -/
  58theorem all_ledgers_are_jcost_critical (L : DefectBoundedSubLedger) : IsJCostCritical L :=
  59  fun δ hδ => by linarith
  60
  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

papers checked against this theorem

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