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

before

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)

  70def before (a b : LedgerSnapshot) : Prop := a.tick.index < b.tick.index

proof body

Definition body.

  71
  72instance : DecidableRel before := fun a b => Nat.decLt a.tick.index b.tick.index
  73
  74/-! ## Arrow of Time: Defect Monotonicity -/
  75
  76/-- **Core Principle**: Within a single epoch, the defect is non-increasing.
  77    Recognition events reduce defect (move toward the cost minimum).
  78    This is what gives time its direction. -/

used by (32)

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

… and 2 more

depends on (17)

Lean names referenced from this declaration's body.