coordAtomicStep
plain-language theorem explainer
coordAtomicStep defines the predicate on pairs of vectors in Z^d such that y differs from x by exactly one coordinate changed by +1 or -1. Ledger-to-parity bridge work in Recognition Science cites this as the atomic update relation that feeds one-bit difference theorems. The definition is introduced directly by the existential quantifier over the changed index k together with the agreement condition on all other coordinates.
Claim. For vectors $x,y : {Z}^d$, the predicate holds precisely when there exists an index $k$ such that $y_k = x_k + 1$ or $y_k = x_k - 1$ and $y_i = x_i$ for every $i ≠ k$.
background
The module supplies the mathematical core of the ledger-to-parity bridge (Workstream B2). It treats integer vectors and their parity patterns (mod 2) as abstract objects; the claim that actual ledger states obey the atomic-step hypothesis is left to a separate theorem. Upstream, parity is the abbrev that applies parityPattern to the phi-vector of a LedgerState, while the various one constants supply the unit increments used in the ±1 clause.
proof idea
This is a definition, not a derived statement. It is introduced by the explicit existential quantifier over the single changed coordinate k, the disjunction for the ±1 difference at that coordinate, and the universal quantifier enforcing agreement elsewhere.
why it matters
The definition supplies the hypothesis for the downstream theorem coordAtomicStep_oneBitDiff, which establishes OneBitDiff between the parity patterns of x and y. It also appears in the abbrev ledgerVecStep and in the posting lemma phiVec_coordAtomicStep_of_post. In the Recognition framework it closes the first half of the ledger-parity adjacency link; the second half (that RS ledger legality forces atomic steps) remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.