dimension_sum_triangular
plain-language theorem explainer
The sum of the fundamental representation dimensions of the color, weak, and hypercharge layers extracted from the 3-cube automorphism group equals the third triangular number 6. A physicist reconstructing the Standard Model gauge structure from hyperoctahedral symmetry B3 would cite this to confirm the layer dimensions exhaust the triangular count of face-pair interactions. The proof is a direct numerical substitution of the layer constants.
Claim. Let the three gauge layers be extracted from the automorphism group of the 3-cube. Then the sum of their fundamental representation dimensions satisfies $3 + 2 + 1 = 6$, which equals the third triangular number $D(D+1)/2$ for $D=3$.
background
The module derives the Standard Model gauge group SU(3) × SU(2) × U(1) from the hyperoctahedral group B3 of the 3-cube Q3, whose vertices are {0,1}^3 and whose order is 48. B3 decomposes into three layers: axis permutations S3 (order 6) for color, even sign flips (Z/2Z)^2 (order 4) for weak, and the remaining sign structure for hypercharge. The referenced layer definitions assign fund_rep_dim values 3, 2, and 1 respectively, matching the Weyl groups of the corresponding factors. Upstream results supply the discrete structures for nuclear densities and J-calibration that frame the overall Recognition Science derivation of gauge structure from cube symmetry.
proof idea
The proof is a one-line wrapper that applies norm_num to the three layer definitions, substituting the constants fund_rep_dim := 3, 2, 1 directly into the left-hand side and reducing the right-hand side 3*(3+1)/2 to 6.
why it matters
This equality verifies that the three layers from B3 = (Z/2Z)^3 ⋊ S3 together saturate the triangular number T(3) = 6 of face-pair interactions required by D = 3 spatial dimensions in the forcing chain. It closes the dimension count in the module's derivation of the full gauge group from cube symmetry, linking the S3 Weyl action to SU(3) color and the even-sign subgroup to SU(2) × U(1). No downstream theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.