cube_gauge_ranks
plain-language theorem explainer
The cube-derived gauge rank function maps each of the three indices to the fundamental representation dimension of one gauge layer extracted from the 3-cube automorphism group. It produces the ordered values 3, 2, 1 for the color, weak, and hypercharge sectors. Researchers reconstructing the Standard Model gauge group from cube symmetries cite this when confirming the rank match to SU(3) × SU(2) × U(1). The definition is a direct finite enumeration of the precomputed layer dimensions.
Claim. The function $r : [3] → ℕ$ defined by $r(0) = 3$, $r(1) = 2$, $r(2) = 1$, where the values are the fundamental representation dimensions of the color, weak-isospin, and hypercharge layers obtained from the signed-permutation decomposition of the 3-cube automorphism group.
background
The module P-014 derives the Standard Model gauge group SU(3) × SU(2) × U(1) from the automorphism group B₃ of the 3-cube Q₃, which decomposes as (ℤ/2ℤ)³ ⋊ S₃. Axis permutations (S₃) supply the color structure, even sign flips supply the weak structure, and the remaining generator supplies hypercharge. A GaugeLayer record holds a name string, the fundamental representation dimension, and the discrete order of the corresponding finite group. The three sibling definitions color_layer, weak_layer, and hypercharge_layer supply the concrete values (3,6), (2,4), and (1,2).
proof idea
One-line wrapper that directly indexes the fundamental representation dimensions of color_layer, weak_layer, and hypercharge_layer into a Fin 3 → ℕ function.
why it matters
The definition supplies the rank tuple required by the matching theorem cube_matches_sm and the gauge group certificate, which together close the P-014 derivation. It connects the T8-forced three spatial dimensions to the gauge ranks that appear in the Yang-Mills mass gap certificate and the forcing-chain theorem mass_gap_from_forcing_chain. The ranks sum to six, matching the face count of Q₃.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.