present
plain-language theorem explainer
The definition selects the ledger state at the current tick from an indexed sequence of states. Foundational work on time emergence from cost minimization cites this to distinguish the present from committed past entries. It is implemented by direct indexing into the state function.
Claim. For a function $s : ℕ → S$ where $S$ is the type of ledger states at ticks, and for current index $n ∈ ℕ$, the present state is $s(n)$.
background
The module formalizes time emergence from ledger updates, identifying time with the tick counter rather than a background parameter. A ledger snapshot consists of a tick index together with a nonnegative defect value measuring deviation from the cost minimum. The present is the snapshot at the active tick, while past entries are those with smaller indices.
proof idea
One-line wrapper that applies the state sequence at the supplied tick index.
why it matters
This definition supports downstream results on baryogenesis trajectories and alpha coordinate fixation by providing the current state for ratio calculations. It fills the F-004 registry item on the nature of time and aligns with the eight-tick cycle forced by spatial dimension three. It is referenced in irreversibility arguments showing recognition proceeds in one direction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.