dimension_sum
plain-language theorem explainer
The fundamental representation dimensions of the color, weak, and hypercharge layers extracted from the hyperoctahedral group B3 sum exactly to the face count of the 3-cube. Researchers deriving the Standard Model gauge group from geometric symmetries would cite this equality to close the dimensional accounting. The proof is a direct numerical evaluation that confirms 3 + 2 + 1 equals 6.
Claim. Let $d_c$, $d_w$, $d_h$ be the fundamental representation dimensions of the color, weak, and hypercharge layers. Then $d_c + d_w + d_h = 6$, where 6 equals the number of faces of the three-dimensional cube.
background
The module derives the Standard Model gauge group SU(3) × SU(2) × U(1) from the automorphism group B3 of the 3-cube Q3, whose elements are signed permutations of three axes. GaugeLayer is a structure recording a name, fund_rep_dim, and discrete_order for each layer. color_layer sets fund_rep_dim to 3 from axis permutations, weak_layer sets it to 2 from even sign flips, and hypercharge_layer sets it to 1 from parity. cube_face_count D is defined as 2D, so the case D = 3 yields 6 faces.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the arithmetic identity 3 + 2 + 1 = 6.
why it matters
This theorem closes the dimensional sum in the module's derivation of the gauge group from cube symmetry, confirming that the three layers exhaust the six faces of Q3 as 3 face-pairs plus 2 couplings plus 1 parity. It directly supports the module claim that the decomposition is not coincidental. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.