RecognitionStep

formal source

 103
 104/-- A recognition event transforms a state by reducing its defect.
 105    This is fundamentally one-way: you cannot "un-recognize." -/
 106structure RecognitionStep where
 107  input : LedgerSnapshot
 108  output : LedgerSnapshot
 109  tick_advance : output.tick.index = input.tick.index + 1
 110  defect_reduce : output.defect ≤ input.defect
 111
 112/-- **Theorem**: Recognition is irreversible.
 113    If a step reduces defect from d₁ to d₂ < d₁, there is no step
 114    that goes from d₂ back to d₁ while advancing the tick counter,
 115    because defect is non-increasing along ticks. -/
 116theorem recognition_irreversible (step : RecognitionStep)
 117    (h_strict : step.output.defect < step.input.defect) :
 118    ¬∃ (reverse : RecognitionStep),
 119      reverse.input = step.output ∧
 120      reverse.output.defect = step.input.defect := by
 121  intro ⟨rev, h_in, h_out⟩
 122  have h1 := rev.defect_reduce
 123  rw [h_in] at h1
 124  linarith
 125
 126/-! ## Present, Past, Future -/
 127
 128/-- The present is the current tick. -/
 129def present (states : ℕ → LedgerSnapshot) (now : ℕ) : LedgerSnapshot :=
 130  states now
 131
 132/-- The past is the set of committed ledger entries (earlier ticks). -/
 133def past (states : ℕ → LedgerSnapshot) (now : ℕ) : Set LedgerSnapshot :=
 134  { s | ∃ n, n < now ∧ states n = s }
 135
 136/-- The future is the set of uncommitted entries (later ticks). -/