stepAt
plain-language theorem explainer
stepAt supplies the explicit update rule for an atomic tick on a finite ledger: at each tick t it posts one unit (debit or credit, chosen by sideAt) to the single account selected by the AtomicTick instance. Ledger modelers in Recognition Science cite it when constructing explicit walks in parity space. The definition is a direct composition of the post operation with the account selector and the side schedule.
Claim. Let $d$ be a natural number. Given an AtomicTick instance for the $d$-account recognition structure, a side schedule assigning debit or credit to each tick, a tick $t$, and a ledger state $L$, the updated state is obtained by posting one unit to the account selected for $t$ with the side prescribed at $t$.
background
AccountRS(d) is the recognition structure whose universe is Fin d with the trivial recognition relation. Side is the inductive type with constructors debit and credit. LedgerState(d) is the abbreviation for the ledger type over AccountRS(d). AtomicTick is the class supplying the postedAt predicate together with the uniqueness of the posted account at each tick; accountAt extracts that account by choice. The module sets up posting-style ledger updates so that each tick changes the phi vector by exactly one unit at one coordinate.
proof idea
One-line definition that applies the post operation to L at the account chosen by the AtomicTick instance for tick t, using the side given by the schedule at t.
why it matters
This definition supplies the concrete step function used to prove that each atomic tick induces a one-bit difference in the parity vector (see stepAt_oneBitDiff and stepAt_isPostingStep). It realizes the posting model that connects the ledger formalism to the Gray-code adjacency results. It supports the construction of explicit adjacent walks required for the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.