recognition_irreversible

formal source

 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). -/
 137def future (states : ℕ → LedgerSnapshot) (now : ℕ) : Set LedgerSnapshot :=
 138  { s | ∃ n, n > now ∧ states n = s }
 139
 140/-- **Theorem**: The past is fixed — past defect values cannot change. -/
 141theorem past_is_fixed (states : ℕ → LedgerSnapshot) (now : ℕ)
 142    (s : LedgerSnapshot) (hs : s ∈ past states now) :
 143    ∃ n, n < now ∧ states n = s := hs
 144
 145/-! ## Time Does Not Exist Without Recognition -/
 146