parityPattern
plain-language theorem explainer
The parity pattern definition maps each integer vector in d dimensions to the d-bit string of coordinate parities, with each bit true precisely when the corresponding integer is odd. Ledger adjacency arguments in Recognition Science cite it to reduce single-coordinate updates to one-bit pattern flips. The definition is realized by a direct functional application of the integer oddness predicate to every coordinate.
Claim. For natural number $d$ and vector $x : [d] → ℤ$, the parity pattern of $x$ is the map sending each index $i$ to the Boolean value true if and only if $x_i$ is odd.
background
The LedgerParityAdjacency module supplies the mathematical bridge from ledger vectors to parity observations that underpins Workstream B2. Pattern $d$ is the type of $d$-bit patterns, concretely realized as functions from the finite set of $d$ coordinates to Bool. The supplied definition extracts the parity (odd/even status) of each coordinate of an integer vector, thereby turning any ledger state into an observable bit string. Upstream integer constructions from logic guarantee that the oddness predicate is available and well-behaved inside the formal system.
proof idea
The definition is a one-line wrapper that applies the integer bodd predicate to the value at each coordinate of the input vector.
why it matters
This definition supplies the parity map consumed by the theorem coordAtomicStep_oneBitDiff, which establishes that atomic coordinate steps produce exactly one-bit differences, and by the abbreviation ledgerVecParity that observes parity on ledger vectors. It constitutes the definitional core of the module’s claim that single ±1 updates induce one-bit pattern changes, thereby preparing the reduction from ledger legality to adjacency inside the Recognition Science framework. The construction touches the open question of how formal ledger constraints are to be linked to physical single-bit dynamics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.