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

parity

show as:
view Lean formalization →

The parity abbreviation maps a ledger state L in dimension d to the parity pattern of its phi-vector. Researchers modeling ledger-based computation or information cost would cite this when connecting double-entry updates to one-bit flips. The definition is a direct one-line wrapper applying parityPattern to the output of phiVec.

claimLet $L$ be a ledger state in dimension $d$. The parity of $L$ is the pattern whose $i$-th coordinate is the parity (odd/even status) of the $i$-th entry in the phi-vector of $L$.

background

LedgerState d is defined as Recognition.Ledger over AccountRS d, the type of configurations with debit and credit entries indexed by tick. The phi-vector extracts the net value (debit minus credit) at each coordinate, while parityPattern from LedgerParityAdjacency converts an integer vector $x : Fin d → ℤ$ into a boolean pattern via Int.bodd on each coordinate. This module models a single tick as posting one unit to exactly one account, so the induced phi change is ±1 at one coordinate and the parity pattern flips in exactly one bit.

proof idea

This is a one-line wrapper that applies parityPattern to the phi-vector of the given ledger state.

why it matters in Recognition Science

This definition supplies the explicit link from posting-style ledger updates to the parity one-bit adjacency lemma, feeding downstream structures such as LedgerComputation and SATLedger in ComputationBridge as well as theorems on circuit lower bounds and SAT computation time. It fills the mathematical glue between ledger language and the parity/Gray adjacency results without deriving the posting rule from recognition axioms.

scope and limits

formal statement (Lean)

  63abbrev parity (d : Nat) (L : LedgerState d) : Pattern d :=

proof body

Definition body.

  64  parityPattern (phiVec (d := d) L)
  65
  66/-! ## Posting model -/
  67

used by (40)

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

… and 10 more

depends on (14)

Lean names referenced from this declaration's body.