recognition_axis_counts
plain-language theorem explainer
Recognition-axis counts on the three compact gauge factors are fixed at (3,2,1) for SU(3), SU(2), and U(1). Anyone citing the cube-to-Standard-Model gauge bridge uses this as the axis half of the completion certificate. The proof is a one-line decidability check against the definitional table.
Claim. The recognition-axis count attached to each compact gauge factor equals $3$ for $\mathrm{SU}(3)$, $2$ for $\mathrm{SU}(2)$, and $1$ for $\mathrm{U}(1)$.
background
The module records the first bridge from the forced $B_3$ cube layer skeleton to the Standard Model compact gauge factors. Prior cube work already forces three layer counts: axis permutations $3$, even sign-flip completion $2$, and parity quotient $1$. The compact-completion rule sends those counts to $\mathrm{SU}(3)$ color, $\mathrm{SU}(2)$ weak isospin, and $\mathrm{U}(1)$ hypercharge phase.
Two notions are kept separate: recognition-axis count $(3,2,1)$ with total $6$ (matching the cube face count), versus actual Lie rank $(2,1,1)$ with total $4$. The definition recognitionAxisCount is the pure lookup table assigning those axis numbers to the three factors. This theorem simply freezes that table as a proved conjunction.
proof idea
One-line wrapper: decide discharges the three equalities by evaluating the definitional cases of the recognition-axis count on the three compact factors. No external lemmas are required beyond the inductive definition of that count.
why it matters
This is the axis half of the cube-to-gauge completion certificate. Downstream, gaugeLieCompletionCert packages it with the factor count, axis total $6$, Lie ranks $(2,1,1)$, and Lie-rank sum $4$. The module starts punchlist item P0-S2-01: the first clean bridge from the $B_3$ cube layer skeleton to the compact gauge-factor skeleton.
Framework-wise it sits next to the forced $D=3$ spatial dimensions (T8) and the eight-tick octave (T7), since the cube face count $6$ is what the axis total matches. It does not yet derive hypercharge assignments or fermion representations; those remain later steps on the same bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.