lie_rank_values
plain-language theorem explainer
The compact Standard Model factors SU(3), SU(2), and U(1) have Lie ranks 2, 1, and 1. Anyone assembling the cube-to-gauge completion certificate cites this numerical triple. The proof is a one-line decidability check against the rank table on the three compact factors.
Claim. The Lie ranks of the compact gauge factors are $\operatorname{rank}(\mathrm{SU}(3))=2$, $\operatorname{rank}(\mathrm{SU}(2))=1$, and $\operatorname{rank}(\mathrm{U}(1))=1$.
background
This module opens the P0-S2-01 bridge from the forced 3-cube layer skeleton to the Standard Model compact gauge factors. Prior cube work supplies recognition-axis counts (3,2,1): three axis permutations map to SU(3) color, the even sign-flip completion of order 2 maps to SU(2) weak isospin, and the parity quotient of order 1 maps to U(1) hypercharge phase.
The file deliberately separates two tallies. Recognition-axis count is (3,2,1) with total 6. Lie rank is the actual Cartan rank of each compact factor: SU(3) has rank 2, SU(2) has rank 1, U(1) has rank 1. The local definition of Lie rank is exactly that lookup table on the three-factor enum.
Nothing here yet derives hypercharge assignments or fermion representations; it only records the rank numbers that the completion certificate will package.
proof idea
One-line wrapper: decide evaluates the three equalities against the definitional cases of the Lie-rank table (SU(3) ↦ 2, SU(2) ↦ 1, U(1) ↦ 1). No lemmas are invoked beyond decidable equality on natural numbers.
why it matters
The triple is the Lie-rank half of the cube-to-gauge skeleton. Downstream, the gauge Lie completion certificate plugs these ranks in as its lie_ranks field, alongside axis counts, factor count, and the rank-sum identity that the total is 4.
In the Recognition forcing picture this is the first clean numerical bridge from B₃ layer counts to the compact SM factor list, keeping axis count (total 6) distinct from Cartan rank (total 4). It does not yet touch the full hypercharge or fermion-representation derivation flagged as still open in the module doc. Framework-wise it sits after the D=3 / eight-tick cube forcing (T7–T8) and before any dynamical gauge coupling work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.