ParityIndex
plain-language theorem explainer
Enumerates the nine independent ℤ₂ parity labels of the recognition ledger: four spacetime, three color (SU(3) Cartan), and two generation. Anyone citing the parity count, basis of the parity space, or Gap45 certification uses this type as the index set. As an inductive enumeration with Fintype, the card is definitionally nine.
Claim. There is a finite index type with nine constructors labeling the independent $\mathbb{Z}_2$ parities of the recognition ledger: charge-parity $P_{cp}$, baryon-minus-lepton $P_{B-L}$, hypercharge $P_Y$, tick-reversal $P_T$, three color Cartan sign flips $P_C^{(1)}, P_C^{(2)}, P_C^{(3)}$, and two generation-mixing signs $P_\tau^{(1)}, P_\tau^{(2)}$. Equality is decidable and the type is finite.
background
The NineParities module formalizes the independent $\mathbb{Z}_2$ symmetries that constrain the double-entry recognition ledger under tick reversal and conjugation. Time advances in discrete ticks (the atomic temporal unit); conjugation plus tick reversal flips every admissible parity on a vacuum page.
The nine labels split by origin: four spacetime parities (charge-parity, $B-L$, hypercharge, tick reversal), three color parities from the SU(3) Cartan generators $\lambda_3$, $\lambda_8$, and their diagonal product, and two generation parities from the rank-2 structure of three generations. Tesla's "magnificence of the 9" is read here as this exact independent count, not numerology.
A parity vector is an assignment of $\mathbb{Z}_2$ values to each index. The vacuum assignment is the zero vector. Downstream, the Fintype cardinality of this index set is matched to the parametric parity count at $D=3$.
proof idea
No proof body: this is an inductive type definition. Nine nullary constructors name the parities; DecidableEq, Repr, and Fintype are derived, so finiteness and decidable equality are automatic. Downstream lemmas such as parity_count_eq_nine obtain $\mathrm{card}=9$ by the derived Fintype instance rather than by a separate counting argument.
why it matters
This index set is the spine of the nine-parity story. It feeds parity_count_eq_nine, the standard basis vectors and their nonzero/distinctness lemmas, the spacetime/color/generation classifiers, and the trichotomy that every index falls in exactly one origin class.
In GapDerivation it is the enumeration that parityCount_matches_enumeration equates to the parametric count at $D=3$, and Gap45Cert records parityCount D = Fintype.card ParityIndex alongside dimensionGap D = 45. That gap certification sits on the forcing chain that yields $D=3$ spatial dimensions (T8) and the eight-tick octave (T7).
The type therefore turns the theory-spec claim "nine independent $\mathbb{Z}_2$ parities flip under conjugation and tick reversal" into a machine-checked index set used wherever ledger admissibility or vacuum parity vanishing is stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.