pith. machine review for the scientific record. sign in
structure definition def or abbrev

JCostMinimalCycle

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  84structure JCostMinimalCycle (L : DefectBoundedSubLedger) where
  85  /-- The events in the cycle -/
  86  cycle_events : List RecognitionEvent
  87  /-- The cycle generates a cohomology class (its topological charge) -/
  88  cycle_class : CohomologyClass L
  89  /-- Zero-defect condition: the cycle's J-cost sums to zero
  90      (every debit is matched by a credit — double-entry structure) -/
  91  zero_defect : cycle_class.z_charge = 0 ∨
  92    -- Or: z_charge ≤ 1 (near-zero, within one recognition tick)
  93    cycle_class.z_charge ≤ 1
  94
  95/-! ## Part 2: One Direction — Algebraic ⟹ Hodge -/
  96
  97/-- Every JCostMinimalCycle is a CoarseGrainingStableClass.
  98    This is the easy direction: cost minima always survive coarse-graining,
  99    because zooming out can only reduce (not increase) the defect budget. -/

used by (21)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (22)

Lean names referenced from this declaration's body.