parity_trichotomy
plain-language theorem explainer
Every one of the nine independent ℤ₂ parity indices lies in exactly one source class: spacetime, color, or generation. Anyone citing the 4+3+2 origin split of the recognition ledger's parity count needs this partition. The proof is a finite case split on the inductive index type, closed by simplification of the three membership predicates.
Claim. For every parity index $p$ among the nine independent $\mathbb{Z}_2$ parities of the recognition ledger, exactly one of the following holds: $p$ is a spacetime parity and neither color nor generation; $p$ is a color parity and neither spacetime nor generation; or $p$ is a generation parity and neither spacetime nor color.
background
The NineParities module counts the independent ℤ₂ symmetries that flip under conjugation and tick reversal on the double-entry recognition ledger. The nine indices are
${P_{cp}, P_{B-L}, P_Y, P_T, P_C^{(1)}, P_C^{(2)}, P_C^{(3)}, P_\tau^{(1)}, P_\tau^{(2)}}$.
They arise from three independent sources: 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 of the three-generation structure). The inductive type ParityIndex enumerates these nine constructors. Three Boolean predicates mark membership in each source class: spacetime holds exactly on the first four constructors, color on the three $P_C$ constructors, and generation on the two $P_\tau$ constructors. The module's claim is that Tesla's "magnificence of the 9" is this exact independent parity count, not numerology.
proof idea
Exhaustive case analysis on the nine constructors of the parity-index type. For each constructor, simplification of the three membership predicates reduces the goal to a trivial true/false combination that matches exactly one disjunct of the trichotomy (spacetime-only, color-only, or generation-only). No external lemmas are required beyond the definitions of the three predicates.
why it matters
This is the classification lemma behind the 4+3+2 origin story of the nine ledger parities. It underwrites the arithmetic identity that spacetime (4) plus color (3) plus generation (2) equals nine, which the sibling decomposition theorem records explicitly, and it supports the broader claim that the vacuum page is constrained by exactly nine independent ℤ₂ flips under tick reversal and conjugation. In the Recognition framework it sits in Foundation, adjacent to dimension forcing and ledger forcing: the same ledger whose double-entry balance forces D = 3 and the eight-tick octave also carries this discrete parity structure. No downstream dependents are wired yet in the graph, so the lemma presently serves as local infrastructure for independence and vacuum-vanishing results in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.