sector_dim_sum
plain-language theorem explainer
The theorem states that the dimensions of the four spectral sectors of the 3-cube sum exactly to 8, matching the vertex count of Q3. Researchers deriving gauge groups and fermion counts from binary cube combinatorics would cite it as the numerical closure of the spectral decomposition. The proof is a direct term-mode normalization that evaluates the dimension function and the vertex cardinality definition.
Claim. The sum of the dimensions of the color sector (3), weak sector (2), hypercharge sector (1), and conjugate sector (2) equals $2^3$.
background
SpectralSector is the inductive type with constructors color, weak, hypercharge, and conjugate. Its dimension function assigns 3 to color (from S3 permutations of axes), 2 to weak (from reflections in two axes), 1 to hypercharge (from single-axis parity), and 2 to conjugate (residual). V(D) is the vertex count of the D-dimensional binary cube, defined by V(D) := 2^D. The module derives the Standard Model gauge content and 24 chiral fermions from D = 3 forcing Q3 to have exactly 8 vertices and automorphism group of order 48.
proof idea
The proof is a one-line term that applies norm_num to the definitions of SpectralSector.dim and V, reducing both sides to the concrete integer 8.
why it matters
This theorem supplies the vertex accounting step inside the master theorem spectral_emergence, which certifies that the full Standard Model plus consciousness structure follows from D = 3. It directly realizes the doc-comment claim that the spectral decomposition accounts for every vertex of Q3 and connects T8 (D = 3) to the 8-tick octave and the |Aut(Q3)| = 48 fermion count.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.