lieRank
plain-language theorem explainer
Assigns the classical Cartan ranks of the Standard Model compact factors: rank(SU(3))=2, rank(SU(2))=1, rank(U(1))=1. Cited by anyone separating cube recognition-axis counts from Lie-algebra ranks in the gauge-completion bridge. The body is a three-clause case split on the compact-factor enum.
Claim. The Lie rank of each compact gauge factor selected by the cube-layer completion is $\mathrm{rank}(\mathrm{SU}(3))=2$, $\mathrm{rank}(\mathrm{SU}(2))=1$, and $\mathrm{rank}(\mathrm{U}(1))=1$.
background
The module starts the cube-to-gauge bridge (punchlist P0-S2-01). Prior cube work forces the $B_3$ layer counts: three axis permutations, a two-fold even sign-flip completion, and a one-fold parity quotient. The completion rule sends those counts to the Standard Model compact factors $\mathrm{SU}(3)$, $\mathrm{SU}(2)$, and $\mathrm{U}(1)$.
CompactGaugeFactor is the three-constructor inductive type naming those factors. The module deliberately keeps two tallies apart: recognition-axis counts $(3,2,1)$ totaling $6$, versus Lie ranks $(2,1,1)$ totaling $4$. Lie rank here means the classical Cartan rank ($n-1$ for $\mathrm{SU}(n)$, $1$ for $\mathrm{U}(1)$).
This is only the first skeleton map from cube layers to compact factors; hypercharge embedding and fermion representations are out of scope.
proof idea
Pure definition by exhaustive pattern match on the three constructors of the compact-factor type. No lemmas, no tactics: $\mathrm{SU}(3)\mapsto 2$, $\mathrm{SU}(2)\mapsto 1$, $\mathrm{U}(1)\mapsto 1$. Downstream theorems re-export the values by decide.
why it matters
Supplies the rank table used by the packaged equalities that the ranks are $(2,1,1)$ and that their sum is $4$, and by the completion certificate structure that records factor count and axis counts. Those objects are the clean bookkeeping layer of the cube-to-gauge bridge: recognition axes stay $(3,2,1)$ while Cartan ranks stay $(2,1,1)$.
In the broader Recognition chain the three spatial axes are forced at T8 ($D=3$), so the cube skeleton is not free input. This definition does not yet close hypercharge or fermion reps; it only pins the rank side of the compact-factor skeleton so later certificates can quote a single total of four.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.