stepAt
stepAt constructs the successor ledger state by applying a single post of one unit debit or credit to the account selected at tick t by the AtomicTick instance, using the side prescribed by the schedule function. Ledger modelers in the parity-adjacency setting cite it to generate explicit tick sequences whose parity vectors differ in exactly one bit. The definition reduces directly to a call of the post operation on the accountAt selector and the supplied side.
claimLet $d$ be a natural number equipped with an AtomicTick instance on the $d$-account recognition structure. For a side schedule $s : {0,1,2,ldots} → {debit, credit}$, a time $t$, and ledger state $L$, the updated state is the result of posting one unit on side $s(t)$ to the unique account posted at tick $t$.
background
AccountRS d is the minimal recognition structure whose universe is the finite set Fin d of d accounts. Side is the inductive type with constructors debit and credit. LedgerState d is the abbreviation for the recognition ledger built over AccountRS d. AtomicTick, imported from Chain, is the class asserting that each tick posts to exactly one unique account via the postedAt predicate and unique_post axiom. The module documentation states that this posting model upgrades vector lemmas to an explicit ledger-shaped evolution that induces one-bit changes in the parity vector, supplying the missing glue to the parity adjacency results.
proof idea
The definition is a one-line wrapper that applies the post primitive to the input ledger at the account returned by accountAt t using the side from the schedule at t.
why it matters in Recognition Science
This definition supplies the concrete step function invoked by the downstream lemmas stepAt_isPostingStep and stepAt_oneBitDiff, which establish that each update is a PostingStep and therefore produces a one-bit difference in the parity vector. It fills the explicit ledger-evolution slot in the module's Workstream B model connecting ledger language to parity/Gray adjacency. In the Recognition framework it supports construction of walks in parity space aligned with the forcing chain and eight-tick octave.
scope and limits
- Does not prescribe how the side schedule is chosen or generated.
- Does not establish conservation of total log-ratio or other global invariants.
- Does not derive the posting rule from more primitive axioms or recognition primitives.
- Does not address multi-tick trajectories or continuous-time limits.
Lean usage
theorem use_stepAt {d : Nat} [AtomicTick (AccountRS d)] (sideAt : Nat → Side) (t : Nat) (L : LedgerState d) : OneBitDiff (parity d L) (parity d (stepAt sideAt t L)) := stepAt_oneBitDiff sideAt t Lformal statement (Lean)
1012noncomputable def stepAt {d : Nat} [AtomicTick (AccountRS d)] (sideAt : Nat → Side) (t : Nat) (L : LedgerState d) :
1013 LedgerState d :=
proof body
Definition body.
1014 post L (accountAt (d := d) t) (sideAt t)
1015