rank_length
plain-language theorem explainer
The length of the rank decomposition list equals three. Researchers deriving the hyperoctahedral group B3 from the three-cube in Recognition Science cite this when confirming the (3,2,1) partition structure. The fact aligns the subgroup ranks with spatial dimension D. The proof is a direct decision procedure on the explicit list definition.
Claim. The length of the list $[3, 2, 1]$ equals $3$.
background
The module establishes the symmetry group of the 3-cube Q3 as the hyperoctahedral group B3, with order 48 obtained from 2^D times D!. The rank decomposition is the list [3, 2, 1], drawn from the gauge ranks SU(3), SU(2), and U(1). Upstream, the (3,2,1) partition is the unique decreasing partition of 6 into 3 parts where the first part equals D = 3.
proof idea
One-line wrapper that applies the decide tactic to the equality on the length of the explicit list [3, 2, 1].
why it matters
This anchors the rank structure inside the cubic symmetry group derived from Recognition Science. It supports the (3,2,1) decomposition that matches the gauge factors to spatial dimension, consistent with the forcing chain step T8 that forces D = 3. The declaration closes a basic structural fact needed for later order computations such as |B3| = 48.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.