pith. machine review for the scientific record. sign in
def definition def or abbrev high

parityPattern

show as:
view Lean formalization →

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.

claimFor 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  27def parityPattern {d : Nat} (x : Fin d → ℤ) : Pattern d :=

proof body

Definition body.

  28  fun i => Int.bodd (x i)
  29
  30/-! ## “Atomic coordinate update” hypothesis -/
  31
  32/-- `y` is obtained from `x` by changing exactly one coordinate by ±1. -/

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (13)

Lean names referenced from this declaration's body.