no_alternative_321
plain-language theorem explainer
The theorem shows that the 3-cube's automorphism group B3 admits no gauge layer fundamental representation dimensions other than the Standard Model tuple (3,2,1). Researchers deriving gauge groups from discrete geometry would cite this result to exclude alternatives such as (4,2,1) or (3,3,1). The proof is a one-line simplification that evaluates the explicit layer definitions.
Claim. The 3-cube does not support gauge layers with fundamental representation dimensions other than (3,2,1). In particular, $¬(dim_{color}=4) ∧ ¬(dim_{weak}=3) ∧ ¬(dim_{hypercharge}=2)$, where the dimensions are those extracted from the signed-permutation layers of the hyperoctahedral group $B_3$.
background
The module derives SU(3) × SU(2) × U(1) from the automorphism group B3 of the 3-cube Q3, the hyperoctahedral group of order 48 acting by signed permutations on ℤ³. B3 decomposes into three layers: axis permutations (S3, order 6) giving the color structure, even sign flips ((ℤ/2ℤ)², order 4) giving the weak structure, and the parity map giving hypercharge. The layer definitions assign fund_rep_dim values 3, 2, and 1 respectively, with the module noting that only these match the forced D=3 and the subgroup orders of B3.
proof idea
The proof is a one-line wrapper that applies simplification to the definitions of color_layer, weak_layer, and hypercharge_layer. These definitions directly set fund_rep_dim to 3, 2, and 1, so the negated equalities hold by direct evaluation.
why it matters
This theorem completes the gauge-structure argument in the module by ruling out all listed alternatives to the Standard Model rank tuple. It fills the explicit gap stated in the doc-comment: (4,2,1) would require D=4 (contradicting the forced three dimensions), (3,3,1) would require six even sign flips (but B3 has only four), and (3,2,2) would require parity order 4 (but the parity kernel has order 2). It supports the claim that only the (3,2,1) layers arise from cube symmetry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.