ledgerVecParity
plain-language theorem explainer
ledgerVecParity extracts the coordinatewise parity pattern from any integer vector state of dimension d. Workers establishing one-bit adjacency under atomic ledger steps cite this map when reducing vector updates to pattern differences. The definition is realized as a direct one-line wrapper delegating to the parityPattern function.
Claim. The parity map $p_d : (Fin d → ℤ) → (Fin d → Bool)$ is given by $p_d(x)_i = (x_i mod 2)$, where the codomain is interpreted as the boolean pattern type.
background
LedgerVecState d is the type Fin d → ℤ, a minimal model of ledger states as integer vectors whose steps are governed by coordAtomicStep. parityPattern converts such a vector to Pattern d by sending each coordinate through Int.bodd, yielding a boolean vector that records odd/even status. The module develops the mathematical core of the ledger-to-parity-to-one-bit-adjacency bridge, with the explicit hygiene note that the present results concern only integer vectors and parity, not yet RS ledger legality.
proof idea
This definition is a one-line wrapper that applies parityPattern to the input state.
why it matters
ledgerVecParity supplies the observation map required by the downstream theorem ledgerVecStep_oneBitDiff, which concludes OneBitDiff (ledgerVecParity d x) (ledgerVecParity d y) from the atomic step hypothesis. It therefore occupies the central position in the module's scaffold for Workstream B2, converting single-coordinate ±1 updates into single-bit pattern flips. The construction remains a pure statement about vectors and does not yet incorporate the separate theorem that RS cost minimization forces the atomic-update hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.