arrow_well_defined

formal source

  90/-- **Theorem (F-006)**: The arrow of time is well-defined.
  91    If defect decreases along the tick sequence, the temporal
  92    ordering and the thermodynamic arrow agree. -/
  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
  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." -/
 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