ledgerVecStep
plain-language theorem explainer
ledgerVecStep defines the atomic step relation on d-dimensional ledger vector states, where a transition from x to y occurs precisely when exactly one coordinate changes by +1 or -1. Researchers building parity-adjacency lemmas in the Recognition Science ledger model cite this to link vector updates to one-bit parity flips. The definition is a direct one-line alias to the coordAtomicStep predicate.
Claim. Let $d$ be a natural number. For states $x, y : (Fin d) → ℤ$, the relation holds if and only if there exists a coordinate $k$ such that $y(k) = x(k) + 1$ or $y(k) = x(k) - 1$, and $y(i) = x(i)$ for all $i ≠ k$.
background
LedgerVecState d is the type of integer vectors Fin d → ℤ that serve as the minimal model for ledger states. coordAtomicStep is the predicate asserting that y differs from x by a single ±1 change in exactly one coordinate while all others remain fixed. The module supplies the mathematical core of Workstream B2: a theorem about integer vectors and parity that states if a ledger-like state changes by a single atomic ±1 update in exactly one coordinate, then the induced parity pattern changes in exactly one bit. Upstream results include the canonical arithmetic object from ArithmeticOf and the non-resonant schedule from Gap45.Beat, which supply the underlying integer and cycle structure.
proof idea
The definition is a one-line wrapper that directly applies the coordAtomicStep predicate to the input states x and y.
why it matters
This definition is the immediate premise for the theorem ledgerVecStep_oneBitDiff, which concludes that an atomic step produces a one-bit difference between the parity patterns of x and y. It fills the bridge-lemma scaffold in the LedgerParityAdjacency module, separating the pure vector-parity fact from any later claim that RS ledger legality plus cost minimization forces single-coordinate updates. The construction stays within the integer-vector setting and does not yet invoke the phi-ladder, J-cost, or the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.