pith. machine review for the scientific record. sign in
def definition def or abbrev high

future

show as:
view Lean formalization →

The future declaration defines the set of ledger snapshots whose tick indices exceed the current now. Researchers on time emergence and the arrow of time cite it to isolate uncommitted entries from the fixed past. It is realized as a direct set comprehension over the indexed state sequence.

claimLet $(s_k)_{k∈ℕ}$ be a sequence of ledger snapshots. For current index $n_0$, the future is the set $ { s | ∃ n > n_0 such that s_n = s } $.

background

The module formalizes time as the ledger tick counter with no background continuum. LedgerSnapshot is the structure carrying a tick index and a nonnegative defect value. The companion past definition extracts states with indices strictly below now. Upstream, defect is the J-functional from LawOfExistence, and the 8-tick cycle supplies the minimal update period.

proof idea

This is a definition realized by a one-line set comprehension that collects every snapshot s for which there exists a tick index n strictly larger than now with states n equal to s.

why it matters in Recognition Science

The definition supplies the uncommitted side of the present/past/future partition required by F-006. It is invoked by arrow_of_time, recognition_irreversible, and downstream results including dark_energy_w and vs_multiverse. It anchors the claim that recognition steps are irreversible because only later ticks remain open.

scope and limits

formal statement (Lean)

 137def future (states : ℕ → LedgerSnapshot) (now : ℕ) : Set LedgerSnapshot :=

proof body

Definition body.

 138  { s | ∃ n, n > now ∧ states n = s }
 139
 140/-- **Theorem**: The past is fixed — past defect values cannot change. -/

used by (31)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 1 more

depends on (7)

Lean names referenced from this declaration's body.