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

present

show as:
view Lean formalization →

The definition present selects the ledger snapshot at the current tick index from a sequence of states indexed by natural numbers. It would be cited in any derivation that separates the instantaneous state from committed past entries or uncommitted future ones within the discrete tick model. The definition is a direct index projection with no additional computation.

claimLet $S : ℕ → LedgerSnapshot$ be a sequence of ledger states and let $n ∈ ℕ$ be the current tick index. The present state is defined by $S(n)$.

background

The TimeEmergence module treats time as the ledger tick counter with no independent continuous parameter. LedgerSnapshot is the structure carrying a tick index together with a nonnegative real defect measuring distance from the cost minimum. The module distinguishes present (current tick), past (earlier committed entries), and future (uncommitted entries) and ties the minimal cycle length to the eight-tick octave forced by three spatial dimensions.

proof idea

The definition is a one-line projection that returns the LedgerSnapshot at the supplied now index from the states sequence.

why it matters in Recognition Science

present supplies the instantaneous state required by downstream results including recognition_irreversible and arrow_of_time. It directly implements the F-004 and F-006 registry items on the nature and direction of time. In the Recognition Science chain it anchors T7 (eight-tick octave) and the one-way character of recognition steps that decrease defect toward the phi-ladder minimum.

scope and limits

formal statement (Lean)

 129def present (states : ℕ → LedgerSnapshot) (now : ℕ) : LedgerSnapshot :=

proof body

Definition body.

 130  states now
 131
 132/-- The past is the set of committed ledger entries (earlier ticks). -/

used by (28)

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

depends on (11)

Lean names referenced from this declaration's body.