parity
plain-language theorem explainer
The abbrev parity extracts the parity pattern of a ledger state L in dimension d by composing parityPattern with the phi vector of L. Researchers modeling ledger updates or balanced-parity encodings in computation would cite this definition to link posting rules to one-bit adjacency. It is a direct one-line composition of two sibling definitions.
Claim. For natural number $d$ and ledger state $L$ in dimension $d$, the parity of $L$ is the parity pattern of its phi-vector: the map sending each coordinate $i$ to the odd/even status of the net debit-credit value at $i$.
background
In LedgerPostingAdjacency a LedgerState d is the type Recognition.Ledger (AccountRS d), i.e., a collection of accounts carrying debit and credit entries indexed by tick. The sibling phiVec extracts the integer vector of net phi values (debit minus credit) across the d coordinates. parityPattern, defined in LedgerParityAdjacency, converts any integer vector x : Fin d → ℤ into a Pattern d by returning the boolean parity (Int.bodd) of each coordinate.
proof idea
One-line wrapper that applies parityPattern to phiVec (d := d) L.
why it matters
This definition supplies the parity extraction step required by downstream ledger-based computation structures such as LedgerComputation and SATLedger in ComputationBridge, and by the balanced-parity lower bound circuit_cannot_sense_moat. It completes the posting-model glue between the ledger language and the parity/Gray adjacency results, supporting claims that recognition time for SAT instances is Ω(n) under balanced-parity encoding. It touches the open question of deriving the single-post rule from the recognition axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.