past
The definition identifies the past with the set of all ledger snapshots whose tick index is strictly smaller than the current now. Workers on the arrow of time and ledger irreversibility cite it when partitioning the state sequence into committed and uncommitted parts. The definition is a direct set comprehension that requires no lemmas.
claimLet $past((s_n)_{n∈ℕ},N) := {s | ∃ n < N : s_n = s}$, where each $s_n$ is a LedgerSnapshot carrying a tick index and nonnegative defect.
background
The TimeEmergence module treats time as the discrete tick counter of the ledger rather than a background continuum. A LedgerSnapshot is the structure (tick : Tick, defect : ℝ, defect_nonneg : 0 ≤ defect). The past collects every snapshot whose tick is earlier than the present tick N. This construction rests on the ledger factorization and phi-forcing results that calibrate the J-cost function used to drive defect reduction.
proof idea
One-line definition via set comprehension: the set of all s such that there exists n < now with states n = s. No tactics or upstream lemmas are invoked.
why it matters in Recognition Science
The definition supplies the temporal partition required by past_is_fixed (which proves defect values in the past cannot change) and by the sibling future definition. It directly implements the F-004/F-006 registry items on the nature and direction of time. The same partition appears in downstream arguments for the cosmological constant equation of state and for predictability thresholds in J-cost models.
scope and limits
- Does not introduce a continuous time parameter.
- Does not prove irreversibility of recognition steps.
- Does not specify the ledger update rule that produces the state sequence.
- Does not constrain the defect values inside the snapshots.
Lean usage
theorem past_is_fixed (states : ℕ → LedgerSnapshot) (now : ℕ) (s : LedgerSnapshot) (hs : s ∈ past states now) : ∃ n, n < now ∧ states n = s := hsformal statement (Lean)
133def past (states : ℕ → LedgerSnapshot) (now : ℕ) : Set LedgerSnapshot :=
proof body
Definition body.
134 { s | ∃ n, n < now ∧ states n = s }
135
136/-- The future is the set of uncommitted entries (later ticks). -/