ParityVector
plain-language theorem explainer
A parity vector is an assignment of a bit in $\mathbb{Z}/2\mathbb{Z}$ to each of the nine independent ledger parities. Anyone citing the nine-parity master theorem, Hamming weight, or tick-reversal conjugation works in this type. The declaration is a pure type synonym with no proof content.
Claim. A parity vector is a function from the nine parity indices $\{P_{cp}, P_{B-L}, P_Y, P_T, P_C^{(1)}, P_C^{(2)}, P_C^{(3)}, P_\tau^{(1)}, P_\tau^{(2)}\}$ to $\mathbb{Z}/2\mathbb{Z}$.
background
The module formalizes nine independent $\mathbb{Z}2$ parities that govern the double-entry recognition ledger under tick reversal and conjugation. They split as four spacetime parities ($P{cp}$, $P_{B-L}$, $P_Y$, $P_T$), three color parities from the SU(3) Cartan, and two generation-mixing parities from the rank-2 three-generation structure.
The index type is an inductive with exactly those nine constructors. A parity vector is then the full assignment of a bit to each index: the configuration space of admissible ledger pages under these signs. The vacuum page (all bonds at rung 0 in the gauge-bond sense) is the zero assignment.
This sits in the foundation layer that counts and classifies the discrete symmetries constraining the ledger, before mass-gap or continuum physics is attached.
proof idea
Pure abbreviation: the type of parity vectors is defined to be the function space from the nine-index inductive to $\mathrm{ZMod},2$. No lemmas are applied; no tactics run.
why it matters
This is the ambient type for the whole nine-parity development. Downstream it is the domain of the standard basis vectors, Hamming weight, tick-reversal conjugation (componentwise flip $v\mapsto v+1$), the involution identity for double flip, and the master theorem that packages count, flip, vacuum vanishing, $4+3+2$ decomposition, algebraic independence, and the $2^9=512$ configuration count.
In the Recognition framework it encodes Tesla's "magnificence of the 9" as the exact dimension of independent $\mathbb{Z}_2$ symmetries on the vacuum page of the ledger, not numerology. It is the discrete skeleton on which later forcing-chain and continuum claims sit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.