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

DefectBoundedSubLedger

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)

  56structure DefectBoundedSubLedger where
  57  /-- Recognition events in the sub-ledger -/
  58  events : List RecognitionEvent
  59  /-- Defect = total J-cost of all recognition events -/
  60  defect : ℝ
  61  /-- Defect is bounded (the variety is non-singular) -/
  62  defect_bounded : defect < phi ^ 44
  63  /-- Defect is nonneg (J-cost is always nonneg) -/
  64  defect_nonneg : 0 ≤ defect
  65
  66/-- A cohomology class on a DefectBoundedSubLedger is a real number
  67    (encoding the "charge" of the class in the Z-complexity sense). -/

used by (33)

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

… and 3 more

depends on (30)

Lean names referenced from this declaration's body.