gauge_sector_dim
plain-language theorem explainer
The dimensions of the color, weak, and hypercharge sectors extracted from the automorphism group of the binary cube Q3 sum to six. Physicists reconstructing the Standard Model gauge group from the forced spatial dimension D=3 would cite this result. The proof is a direct numerical reduction on the explicit dimension assignments in the SpectralSector definition.
Claim. $3 + 2 + 1 = 6$, where the three summands are the dimensions of the color, weak, and hypercharge sectors in the decomposition of the automorphism group of the three-dimensional binary cube $Q_3$.
background
The module starts from the forced datum D=3 (T8) that produces the binary cube Q3 with eight vertices. Its automorphism group B3 of order 48 decomposes as S3 ⋉ (Z/2Z)^3 and simultaneously encodes the gauge content of the Standard Model. The SpectralSector inductive type partitions this decomposition into four layers: color from the S3 permutations of the three axes, weak from reflections in two axes, hypercharge from single-axis parity, and a residual conjugate sector.
proof idea
The term-mode proof applies the norm_num tactic to the SpectralSector.dim definitions. These definitions assign the constants 3, 2, and 1 to the color, weak, and hypercharge cases respectively, so the sum evaluates immediately to six.
why it matters
This result supplies the gauge-sector count required by the module's central claim that Q3 forces SU(3) × SU(2) × U(1) content with physical dimension six. It sits inside the self-consistency loop that runs from T8 (D=3) through the eight-tick octave to the observed gauge structure and the 48 chiral fermionic states. No downstream theorems are listed, but the declaration closes one of the explicit numerical identities listed in the module introduction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.