stepAt_isPostingStep
plain-language theorem explainer
The lemma shows that advancing a d-dimensional ledger state via stepAt at tick t under a side schedule yields a valid PostingStep. Ledger modelers working on parity adjacency in Recognition Science cite this to bridge atomic posts to one-bit difference results. The proof is a one-line wrapper that directly supplies the account witness, side, and equality.
Claim. Let $d$ be a natural number. Assume an AtomicTick instance on the account recognition structure of dimension $d$. Let sideAt map natural numbers to debit or credit, let $t$ be a natural number, and let $L$ be a ledger state of dimension $d$. Then the state obtained by stepAt at $t$ on $L$ satisfies the posting-step relation from $L$.
background
AccountRS d is the minimal carrier for a d-account ledger with universe Fin d and trivial recognition relation. LedgerState d abbreviates the Recognition.Ledger over this structure. PostingStep L L' holds precisely when there exist an account k in Fin d and a side such that L' equals the post operation applied to L at k with that side. AtomicTick supplies that each tick t posts to a unique account in the structure. The accountAt function selects this unique account via classical choice from the unique_post axiom. The module models ledger updates as single-unit debit or credit posts to one account, providing the explicit ledger shape needed to connect to parity one-bit adjacency.
proof idea
The proof is a one-line wrapper that applies the existential definition of PostingStep. It refines by supplying the account chosen by accountAt at tick t, the side taken from sideAt at t, and reflexivity to witness equality with the post operation.
why it matters
This lemma feeds directly into stepAt_oneBitDiff, which applies postingStep_oneBitDiff to obtain the one-bit difference on parity vectors. It supplies the glue between the stepAt posting schedule and the parity/Gray adjacency lemma in the same module. In the Recognition framework it realizes the ledger-shaped model that induces adjacent walks in parity space, supporting the transition from atomic ticks to the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.