parity_count_eq_nine
plain-language theorem explainer
There are exactly nine independent ℤ₂ parity indices on the recognition ledger. Anyone citing the nine-parity vacuum structure, the 2⁹=512 configuration count, or the gap-derivation match to D=3 would invoke this count. The proof is a one-line decidability check on the finite inductive enumeration of those indices.
Claim. The finite set of parity indices has cardinality $9$: there are exactly nine independent $\mathbb{Z}_2$ parities labeling the double-entry ledger.
background
The NineParities module enumerates the independent ℤ₂ symmetries that constrain the recognition ledger under tick reversal and conjugation. They split by origin into four spacetime parities (charge-parity, $B-L$, hypercharge, tick reversal), three color parities (Cartan generators of SU(3)), and two generation parities (rank-2 mixing signs from three generations), totaling $4+3+2=9$.
ParityIndex is the inductive type whose nine constructors are exactly those labels. A parity vector assigns a value in $\mathbb{Z}_2$ to each index; the vacuum page is the zero vector. The module's claim is that this count is not numerology but the exact dimension of the independent sign structure of the ledger.
proof idea
One-line decidability proof. Lean has a Fintype instance on the inductive ParityIndex (nine nullary constructors). decide evaluates Fintype.card ParityIndex = 9 by exhaustive computation on that finite type and closes the goal by reflexivity. No algebraic lemmas are required.
why it matters
This is the count axiom of the nine-parity package. It is the first conjunct of the master theorem nine_parities_master (count, flip under conjugation+tick reversal, vacuum vanishing, $4+3+2$ decomposition, algebraic independence, $2^9=512$ states). Downstream, parity_space_dimension is a direct alias, and total_parity_configs rewrites the card of parity vectors through this equality to obtain $512$.
In GapDerivation, parityCount_matches_enumeration identifies the parametric parity count at $D=3$ with this enumeration, tying the foundation count into the gap=$45$ chain. Within the broader forcing picture the nine parities are the discrete sign skeleton of the ledger once $D=3$ and the eight-tick octave are fixed; the theorem simply locks the cardinality that every later configuration or gap argument quotes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.