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 modelers cite the result when reducing coordinate updates to bit-adjacency. The tactic proof cases on the sign of the change, invokes Int.bodd_add to establish the parity toggle at the updated index, and derives uniqueness by contradiction with the unchanged coordinates.
Claim. Let $x,y : [d] → ℤ$. Suppose there exists $k$ such that $y_k = x_k + 1$ or $y_k = x_k - 1$ and $y_i = x_i$ for all $i ≠ k$. Then the parity vectors (coordinate-wise bodd) of $x$ and $y$ differ in exactly one position.
background
The module supplies the mathematical core of Workstream B2: a theorem about integer vectors and parity, not a claim about nature. coordAtomicStep asserts that y is obtained from x by a single ±1 update at one index k with all other coordinates fixed. parityPattern maps each coordinate to its parity via Int.bodd. OneBitDiff A B asserts that A and B differ at exactly one index k and agree elsewhere. The local setting is a bridge lemma scaffold that still requires a separate result linking RS ledger legality to the atomic-update hypothesis.
proof idea
The tactic proof rcases the coordAtomicStep hypothesis to extract index k and the step condition. It refines OneBitDiff to witness k. For the difference at k it splits on +1 versus -1, applies Int.bodd_add (and bodd_neg for the minus case) to show the parity toggles, then rewrites with the step equation. For uniqueness it assumes another differing index i, invokes the rest condition to obtain y_i = x_i, and derives a contradiction with the assumed parity difference.
why it matters
The result is the direct parent of ledgerVecStep_oneBitDiff (a one-line wrapper that unfolds and reapplies the theorem) and is reused in parity_oneBitDiff_of_post after reduction to a coordinate step. It fills the B2 requirement that atomic ±1 ledger updates induce one-bit parity changes, supplying the adjacency link needed for later ledger-parity arguments. It touches the open question whether RS cost-minimization forces the atomic hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.