color_parity_count_from_D3
plain-language theorem explainer
The color sector of the recognition ledger contributes exactly three independent ℤ₂ parities, identified with the forced spatial dimension D=3. The count is justified by SU(3) having rank 2 (two Cartan generators plus one diagonal product). Anyone assembling the nine-parity vacuum page cites this identification. The proof is pure reflexivity: both sides are the numeral 3.
Claim. The number of independent color parities equals $3$, and this equals the forced spatial dimension $D=3$. (SU(3) color has rank $2$, giving two Cartan generators plus one diagonal product.)
background
The module counts nine independent ℤ₂ parities that flip under conjugation and tick reversal on the double-entry recognition ledger. They split into three sources: four spacetime parities (charge-parity, B−L, hypercharge, tick reversal), three color parities, and two generation parities. Tesla’s “magnificence of the 9” is read as this exact algebraic count, not numerology.
Spatial dimension is forced to $D=3$ already in the foundation chain (T8 / linking). Constants modules expose D := 3 and the fundamental tick $\tau_0=1$. Color enters because the SU(3) Cartan subalgebra has rank 2; adjoining the overall diagonal product yields three independent sign flips $P_C^{(1..3)}$.
Upstream dimension and tick definitions therefore supply the numeral that this declaration equates to the color-parity count.
proof idea
Term-mode reflexivity. Both sides of the equality are the literal natural number 3, so rfl closes the goal immediately. No lemmas are applied; the declaration is a named witness that the color count and $D$ share the same numeral.
why it matters
This pins the middle summand in the module’s source decomposition (spacetime 4 + color 3 + generation 2 = 9). The sibling parity_count_eq_nine and the trichotomy/source-decomposition results rely on each block having a fixed cardinality; here the color block is locked to the same 3 that T8 forces for space. The doc-comment explicitly ties the count to SU(3) rank plus diagonal product and to D=3 forcing, so the declaration is the ledger-side echo of the geometric forcing step rather than an independent dynamical claim. With no downstream users yet, it still documents the color contribution required by the nine-parity overview and the theory-spec lines on independent ℤ₂ flips.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.