rankDecomposition
plain-language theorem explainer
rankDecomposition defines the list [3, 2, 1] as the rank structure for the cubic symmetry group B3. Researchers deriving the Standard Model gauge factors from the 3-cube symmetry in Recognition Science cite it to fix the partition into spatial dimension, sub-cube, and phase components. The definition is a direct constant assignment with no proof body or lemmas.
Claim. The rank decomposition is the list $ [3, 2, 1] $.
background
The module derives the cubic symmetry group from the Recognition Science recognition lattice built on the 3-cube Q₃. Its symmetry group is the hyperoctahedral group B₃ whose order is 48, equivalently 2³ × 3!. The (3,2,1) rank decomposition is the unique decreasing partition of 6 into three parts whose largest part equals the spatial dimension D = 3. Upstream the GaugeGroupCube module supplies the matching gauge ranks via the theorem gaugeRankSU3 = 3 ∧ gaugeRankSU2 = 2 ∧ gaugeRankU1 = 1.
proof idea
The definition is a direct literal assignment of the list [3, 2, 1] with no tactics or lemmas applied.
why it matters
This definition supplies the concrete list used by CubicSymmetryCert to assert b3_order = 48, hyperoctahedralOrder 3 = 48, and rank_sum = 6. It also feeds gaugeCubeCert, linking the cubic symmetry directly to the Standard Model gauge ranks. It realizes the T8 step that fixes D = 3 spatial dimensions in the forcing chain and anchors the (3,2,1) structure underlying the alpha band constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.