pith. machine review for the scientific record. sign in
theorem proved term proof

arrow_well_defined

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)

  93theorem arrow_well_defined (states : ℕ → LedgerSnapshot)
  94    (h : DefectMonotone states) (n : ℕ)
  95    (h_step : (states (n + 1)).tick.index = (states n).tick.index + 1) :
  96    arrow_of_time (states n) (states (n + 1)) := by

proof body

Term-mode proof.

  97  constructor
  98  · show (states n).tick.index < (states (n + 1)).tick.index
  99    omega
 100  · exact h.defect_decreasing n h_step
 101
 102/-! ## Irreversibility of Recognition -/
 103
 104/-- A recognition event transforms a state by reducing its defect.
 105    This is fundamentally one-way: you cannot "un-recognize." -/

depends on (24)

Lean names referenced from this declaration's body.