rank_sum
plain-language theorem explainer
The sum of the entries in the (3,2,1) rank decomposition equals 6. Researchers embedding gauge groups into the recognition lattice's cubic symmetry cite this to confirm the total rank matches the required partition. The proof is a one-line decision procedure on the explicit list definition.
Claim. The sum of the entries in the rank decomposition list $[3, 2, 1]$ equals 6.
background
The module derives the cubic symmetry group of the 3-cube Q₃ in the RS recognition lattice. Its symmetry group is the hyperoctahedral group B₃ of order 48, expressed as 2³ × 3!. The rankDecomposition is defined locally as the list [3, 2, 1] that encodes the subgroup rank structure for the gauge factors.
proof idea
The proof is a one-line wrapper that applies the decide tactic directly to the concrete definition of rankDecomposition as [3, 2, 1].
why it matters
This supplies the rank_sum field inside the CubicSymmetryCert structure, which is then used to build the ElectroweakCert in the electroweak unification module. It confirms the total rank sums to 6, consistent with the (3,2,1) partition whose first entry equals spatial dimension D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.