stepAt
plain-language theorem explainer
The atomic tick step function encodes an atomic tick as an explicit post to one account under a debit or credit schedule. Ledger modelers in Recognition Science cite it when constructing parity-adjacent walks from posting sequences. The definition reduces to a single call of the post operation on the account selected by the AtomicTick instance at the given tick.
Claim. Given a natural number $d$ equipped with an AtomicTick instance on the d-account recognition structure, a schedule from naturals to debit or credit, a tick $t$, and a ledger state $L$, the atomic tick step returns the ledger state obtained by posting one unit to the account chosen at tick $t$ with the side given by the schedule at $t$.
background
This module upgrades the ledger model to explicit posting updates that produce one-bit changes in parity. The d-account recognition structure is the minimal carrier whose universe is the finite set with d elements. Debit and credit form the two possible sides for each post. The ledger state is the recognition ledger built over this structure. AtomicTick is the class that declares a unique posted account for each tick, extracted by the account selection function.
proof idea
The definition is a one-line wrapper that applies the post operation to the input ledger state at the account chosen for the tick, using the side from the schedule at that tick.
why it matters
This definition supplies the concrete update rule invoked by the lemmas establishing that each step is a valid posting step and that it produces a one-bit difference in the parity vector. It realizes the module's central claim that a single post alters the debit-credit difference by one at exactly one coordinate. The construction bridges the abstract atomic tick class to explicit ledger trajectories, supporting the parity adjacency results without addressing the physical justification for the posting model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.