present
plain-language theorem explainer
The present definition extracts the ledger snapshot at the current tick from a sequence of states indexed by natural numbers. It supports formalizations of time as discrete ledger updates in Recognition Science. The implementation is a direct index projection with no additional computation.
Claim. Given a map $s : ℕ →$ LedgerSnapshot and current tick $n ∈ ℕ$, the present state is $s(n)$.
background
LedgerSnapshot is the structure holding a tick index together with its defect value (non-negative real). The TimeEmergence module treats time as the ledger tick counter itself, with no external continuous parameter. Present, past, and future are defined relative to the current tick: present is the active snapshot, past consists of committed earlier entries, and the 8-tick cycle (2^D for D=3) supplies the minimal complete update period.
proof idea
One-line wrapper that applies direct indexing into the states sequence at the now parameter.
why it matters
This definition anchors the module's core results on time emergence (F-004, F-006) and feeds downstream lemmas including recognition_irreversible and etaBAt_adjacent_ratio. It realizes the framework identification of time with ledger ticks and the irreversible defect decrease that produces the arrow of time.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.