ledgerVecStep_oneBitDiff
plain-language theorem explainer
A single atomic update in one coordinate of an integer vector changes its parity pattern by exactly one bit. Workers on discrete ledger models or parity-based adjacency relations cite this when connecting vector steps to pattern differences. The proof reduces directly to the coordinate-level result by unfolding the ledger-vector wrappers.
Claim. Let $d$ be a natural number and let $x,y : Fin d → ℤ$ be integer vectors. If $y$ differs from $x$ by changing exactly one coordinate by $+1$ or $-1$ while leaving all others fixed, then the parity patterns of $x$ and $y$ differ in exactly one position.
background
LedgerVecState $d$ is the type of integer vectors indexed by $Fin d$. The relation ledgerVecStep $d$ $x$ $y$ holds precisely when $y$ is obtained from $x$ by a single-coordinate atomic step: there exists $k$ such that $y k = x k ± 1$ and $y i = x i$ for all $i ≠ k$. The map ledgerVecParity $d$ sends such a vector to its parity pattern, the function that records the parity (mod 2) of each coordinate. OneBitDiff $p$ $q$ asserts that the two patterns differ in exactly one coordinate, i.e., there exists a unique $k$ with $p k ≠ q k$ (from the GrayCycle module). The module documentation positions the file as the mathematical core of Workstream B2: a theorem about integer vectors and parity that later requires a separate result linking ledger legality to the atomic-step hypothesis.
proof idea
This is a one-line wrapper. The simpa tactic unfolds the definitions of ledgerVecStep and ledgerVecParity, then directly applies the upstream theorem coordAtomicStep_oneBitDiff to the same $x$, $y$ and hypothesis.
why it matters
The declaration supplies the ledger-vector instance of the one-bit parity change property, completing the bridge from atomic ledger steps to parity adjacency. It fills the role described in the module documentation for Workstream B2, where ledger constraints must imply single-coordinate updates before parity adjacency follows. No downstream uses are recorded, indicating it functions as a foundational interface for subsequent theorems on pattern dynamics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.