stepAt_oneBitDiff
plain-language theorem explainer
A single posting step on a d-account ledger changes the parity vector in exactly one bit. Ledger modelers cite this to connect explicit posting mechanics to Gray-code adjacency. The proof is a one-line wrapper that feeds the concrete stepAt construction into the general posting-step one-bit-diff lemma.
Claim. Let $d$ be a natural number. Assume an atomic tick structure on the $d$-account recognition structure. Given a side assignment from ticks to debit or credit, a tick $t$, and a ledger state $L$, the parity vector of $L$ differs from the parity vector after the posting step at $t$ in exactly one bit.
background
AccountRS d supplies the minimal recognition structure whose universe is Fin d. LedgerState d is the ledger over this structure. Side is the inductive type with constructors debit and credit. AtomicTick is the class asserting that each tick posts to a unique account. The module models a ledger update in which each tick posts exactly one unit to exactly one account, either as debit or credit, thereby shifting the debit-credit difference vector by exactly one unit at one coordinate.
proof idea
The term applies postingStep_oneBitDiff to the result of stepAt_isPostingStep, which establishes that the concrete stepAt call yields a PostingStep instance.
why it matters
This declaration supplies the missing glue between the ledger posting model and the parity one-bit adjacency lemma in LedgerParityAdjacency. It realizes the single-bit change required by the Recognition Composition Law and the eight-tick octave structure. No downstream uses are recorded; the result closes the model-to-parity bridge identified in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.