parity_oneBitDiff_of_post
plain-language theorem explainer
A single unit posting (debit or credit) at one account in a d-dimensional ledger changes the parity pattern of the associated phi vector in exactly one bit. Ledger modelers in recognition science cite this result to establish adjacency between consecutive states under atomic updates. The proof obtains the coordinate atomic step property from the post definition and applies the general one-bit difference theorem for such steps.
Claim. Let $L$ be a ledger state over $d$ accounts. For any account index $k$ and side $s$ (debit or credit), if $L'$ is the state obtained by applying one unit post at $k$ on side $s$, then the parity pattern of $L$ differs from the parity pattern of $L'$ in exactly one bit.
background
In the LedgerPostingAdjacency module a LedgerState d is the Recognition.Ledger carrier over AccountRS d, whose universe is Fin d. The post operation increments either the debit or credit component by one at a chosen account k. phiVec extracts the integer vector of recognition values (debit minus credit) across accounts, while parity d L computes the parity pattern of that vector. Upstream, coordAtomicStep asserts that one vector is obtained from another by altering exactly one coordinate by ±1, and the theorem coordAtomicStep_oneBitDiff proves this yields a one-bit difference in the corresponding parity patterns.
proof idea
The proof is a one-line wrapper. It invokes phiVec_coordAtomicStep_of_post to obtain the required coordAtomicStep instance on the phiVec values, then applies coordAtomicStep_oneBitDiff to conclude the one-bit parity difference.
why it matters
This theorem supplies the core adjacency property for single posting steps and is invoked directly by postingStep_oneBitDiff (for general PostingStep relations) and run_step_oneBitDiff (for iterated runs). It completes the bridge from explicit ledger posting semantics to the parity adjacency results of LedgerParityAdjacency, supporting the ledger-shaped model required by the Recognition framework. It touches the open modeling question of how atomic updates produce controlled parity changes, consistent with the eight-tick octave and D=3 constraints in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.