coordAtomicStep_oneBitDiff
plain-language theorem explainer
If vector y differs from x by exactly one coordinate changed by ±1, then the parity patterns of x and y differ in exactly one bit. Ledger and cellular-automaton proofs cite this result to convert atomic updates into one-bit adjacency statements. The proof splits on the sign of the update, invokes the bodd toggle property for ±1, and closes uniqueness by contradiction on any other differing index.
Claim. If $y$ is obtained from $x$ by changing exactly one coordinate by $+1$ or $-1$, then the parity vectors (componentwise odd/even) of $x$ and $y$ differ in precisely one position.
background
The module supplies the mathematical core of Workstream B2: a ledger-like integer vector changes by a single atomic ±1 update in one coordinate if and only if its parity pattern (the vector of Int.bodd values) changes in exactly one bit. coordAtomicStep is the predicate asserting that y differs from x at precisely one index k by ±1 while all other coordinates remain fixed. parityPattern maps each coordinate to its parity bit. OneBitDiff asserts that two vectors differ at exactly one index. The local setting is a minimal ledger-state model whose steps are required to be atomic coordinate updates; turning this into a physical claim still needs a separate theorem that RS ledger legality forces such atomic steps.
proof idea
The tactic proof begins with classical and rcases on the coordAtomicStep hypothesis to extract the changed index k and the sign of the update. It then splits into two cases. For +1 it applies Int.bodd_add to obtain the toggle bodd(z+1) = xor (bodd z) true and rewrites to show the parities differ at k. For -1 it rewrites z-1 as z+(-1), again uses bodd_add together with bodd(-1)=true, and obtains the same toggle. Uniqueness is proved by contradiction: if another index i differs in parity then the rest hypothesis forces y i = x i, hence equal parities, contradicting the OneBitDiff assumption.
why it matters
The result is invoked directly by ledgerVecStep_oneBitDiff (which lifts it to LedgerVecState) and by parity_oneBitDiff_of_post (which reduces a unit debit/credit post to an atomic coordinate step). It therefore supplies the central bridge lemma for the B2 adjacency scaffold: atomic ledger updates imply one-bit parity flips. In the Recognition framework this supports the claim that ledger legality plus cost minimization yields adjacency in the parity graph, a prerequisite for the eight-tick octave and D=3 spatial structure. No open scaffolding remains inside this file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.