future
plain-language theorem explainer
The future function maps a ledger state sequence and current tick index to the set of snapshots whose ticks lie strictly later. Researchers formalizing the arrow of time or ledger irreversibility cite it when partitioning committed versus uncommitted entries. The definition is a direct set comprehension selecting states by tick index.
Claim. Let $states : ℕ → LedgerSnapshot$ be a sequence of ledger states indexed by ticks and let $now : ℕ$ be the present tick. Then $future(states, now)$ denotes the set of all $s$ such that there exists $n > now$ with $states(n) = s$.
background
The module formalizes time emergence from the ledger update cycle. Time is identified with the tick counter; there is no external continuous parameter. A LedgerSnapshot is a structure carrying a tick index together with a nonnegative defect value. The companion definition past extracts the set of states with tick index strictly less than now, so that present, past, and future partition the sequence.
proof idea
One-line definition via set comprehension that selects states whose tick index exceeds now.
why it matters
The definition supplies the future half of the temporal partition required by the arrow-of-time results (F-006) in the same module. It is referenced by the past definition and appears in downstream ledger-based arguments on irreversibility and defect monotonicity. The construction rests on the eight-tick octave and the fact that defect decreases only toward the cost minimum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.