JCostGradient

formal source

  41
  42/-- The J-cost gradient: how much the total defect changes when we perturb
  43    a recognition event by a small amount. At a minimum, this is zero. -/
  44structure JCostGradient (L : DefectBoundedSubLedger) where
  45  /-- The gradient value (defect change per unit perturbation) -/
  46  value : ℝ
  47  /-- Computable from the recognition events: δJ/δeᵢ for each event eᵢ -/
  48  event_count : L.events.length
  49
  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