past

formal source

 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
 147/-- **Theorem (F-004 core)**: Time is not a background parameter.
 148    Time is DEFINED as the tick count. Without ledger updates, there is no time.
 149    The tick count is a natural number, not a real number.
 150    Continuous time is an approximation valid only for large tick counts. -/
 151theorem time_is_discrete : epoch_length = 2 ^ (3 : ℕ) := by
 152  simp [epoch_length, DimensionForcing.eight_tick]
 153
 154/-- **Theorem**: The minimal temporal resolution is one tick.
 155    No sub-tick dynamics exist. Events are quantized in time. -/
 156theorem minimal_temporal_resolution :
 157    ∀ (s₁ s₂ : LedgerSnapshot),
 158    before s₁ s₂ → 1 ≤ s₂.tick.index - s₁.tick.index := by
 159  intro s₁ s₂ h
 160  unfold before at h
 161  omega
 162
 163/-! ## Summary Certificate -/