`before`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.TimeEmergence
domain: Foundation
line: 70 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.TimeEmergence on GitHub at line 70.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  67  defect_nonneg : 0 ≤ defect
  68
  69/-- Temporal ordering: snapshot A is before snapshot B iff its tick index is smaller. -/
  70def before (a b : LedgerSnapshot) : Prop := a.tick.index < b.tick.index
  71
  72instance : DecidableRel before := fun a b => Nat.decLt a.tick.index b.tick.index
  73
  74/-! ## Arrow of Time: Defect Monotonicity -/
  75
  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.