DefectMonotone

formal source

  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. -/
  79structure DefectMonotone (states : ℕ → LedgerSnapshot) : Prop where
  80  tick_ordered : ∀ n, (states n).tick.index ≤ (states (n + 1)).tick.index
  81  defect_decreasing : ∀ n,
  82    (states (n + 1)).tick.index = (states n).tick.index + 1 →
  83    (states (n + 1)).defect ≤ (states n).defect
  84
  85/-- The arrow of time is the direction of defect decrease.
  86    Time "flows" from higher defect to lower defect. -/
  87def arrow_of_time (s₁ s₂ : LedgerSnapshot) : Prop :=
  88  before s₁ s₂ ∧ s₂.defect ≤ s₁.defect
  89
  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