isGenerationParity
plain-language theorem explainer
Marks which of the nine ledger ℤ₂ parity indices are generation parities: exactly the two generation-mixing signs P_τ^{(1)} and P_τ^{(2)}. Anyone partitioning the nine parities by origin (spacetime / color / generation) cites this predicate. It is a pure case split on the parity index type.
Claim. A parity index $p$ is a generation parity precisely when $p\in\{P_\tau^{(1)},P_\tau^{(2)}\}$; for every other index the predicate is false.
background
The module formalizes nine independent ℤ₂ parities of the recognition ledger under tick reversal and conjugation: ${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 sources: four spacetime parities, three color parities (SU(3) Cartan), and two generation parities.
The generation pair comes from the three-generation structure (rank 2): two independent generation-mixing sign flips. The ambient type is the inductive ParityIndex with nine constructors, two of which are the generation labels $P_{\tau1}$ and $P_{\tau2}$.
Sibling classifiers isSpacetimeParity and isColorParity play the same role for the other two source buckets. Together they feed the trichotomy that every index sits in exactly one bucket.
proof idea
Definition by exhaustive pattern match on the parity index: true on the two generation constructors, false on the other seven. No lemmas, no tactics; the body is the classifying equation.
why it matters
Closes the generation leg of the three-source decomposition of the nine ledger parities. Downstream, parity_trichotomy uses it (with the spacetime and color classifiers) to prove every parity belongs to exactly one source category, by cases and simplification.
In the broader Recognition picture this is the "2" in the 4+3+2 split that makes Tesla's nine concrete: nine independent ℤ₂ symmetries constraining the vacuum page, not numerology. It does not itself prove independence or the flip-under-tick-reversal law; those live in sibling theorems (parity_independence, parities_flip_under_tick_reversal).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.