generation_parity_count
plain-language theorem explainer
Exactly two independent generation parities exist: three forced generations minus one overall phase leave two relative mixing signs. Anyone counting the nine ledger ℤ₂ symmetries cites this as the generation contribution. The proof is reflexivity on the arithmetic identity 2 = 2.
Claim. The generation sector contributes exactly two independent $\mathbb{Z}_2$ parities. They arise as $3-1=2$ relative phases among three generations, the three generations themselves forced by the eight-tick structure ($2^3=8$).
background
The module NineParities formalizes nine independent $\mathbb{Z}_2$ symmetries 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 split by source: four spacetime parities, three color parities (SU(3) Cartan), and two generation parities. The generation pair $P_\tau^{(1)}, P_\tau^{(2)}$ is the rank-2 residual after removing the overall phase from three generations.
Three generations are not free parameters. The eight-tick octave (forcing chain T7: period $2^3$) supplies $\log_2 8 = 3$ independent generation slots; the relative-phase count is then $3-1=2$. Adjacent results in the module record the total count nine and the trichotomy of sources.
proof idea
Term-mode reflexivity: the statement is literally $2=2$, discharged by rfl. No lemmas are applied. The theorem exists only as a named, citable record of the generation contribution inside the nine-parity inventory; the arithmetic and the forcing story live in the doc-comment and in the surrounding source-decomposition results.
why it matters
This is the generation leg of the three-source decomposition that yields Tesla's nine: spacetime (4) + color (3) + generation (2). It sits beside parity_count_eq_nine, isGenerationParity, and source_decomposition in the same module. Framework landmark T7 (eight-tick octave) is the reason the generation count is three rather than free, so the residual parity rank is forced to two. Downstream the nine parities constrain which ledger configurations remain admissible under conjugation and tick reversal; a scalar vacuum page must have all nine vanishing. No parent theorem currently imports this declaration (used_by is empty), so its role is documentary and inventory-level rather than a proof dependency.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.