recognition_axis_total
plain-language theorem explainer
The recognition-axis counts on the three compact gauge factors sum to the face count of the 3-cube: 3+2+1=6. Anyone citing the cube-to-Standard-Model gauge bridge uses this identity. The proof rewrites the right-hand side by the known D=3 face count and closes by decidable arithmetic.
Claim. The recognition-axis counts attached to the compact factors satisfy $n_{\mathrm{SU}(3)}+n_{\mathrm{SU}(2)}+n_{\mathrm{U}(1)}=3+2+1$, and this equals the number of faces of the $3$-cube, namely $2\cdot 3=6$.
background
This module records the first bridge from the forced $B_3$ cube layer skeleton to the Standard Model compact gauge factors. Recognition-axis counts are the integers $(3,2,1)$ carried by $\mathrm{SU}(3)$, $\mathrm{SU}(2)$, and $\mathrm{U}(1)$ respectively; they are kept separate from the Lie ranks $(2,1,1)$. The assignment is the compact-completion rule $3\mapsto\mathrm{SU}(3)$ color, $2\mapsto\mathrm{SU}(2)$ weak isospin, $1\mapsto\mathrm{U}(1)$ hypercharge phase.
Upstream, the $D$-cube face count is defined by $\mathrm{cube_face_count}(D)=2D$ (equivalently $D$ opposite pairs). Specializing to three spatial dimensions yields the theorem that the $3$-cube has six faces. That six matches the total recognition-axis budget is the content here. The local setting is the punchlist item that starts from forced $B_3$ layer counts (axis permutations $3$, even sign-flip completion $2$, parity quotient $1$) and packages them as compact gauge factors; full hypercharge and fermion representations are deferred.
proof idea
One short tactic proof. Rewrite the right-hand side with the upstream theorem that the $3$-cube has six faces, reducing the goal to $3+2+1=6$. Close by decide on the concrete natural-number arithmetic coming from the recognition-axis count definition ($\mathrm{SU}(3)\mapsto 3$, $\mathrm{SU}(2)\mapsto 2$, $\mathrm{U}(1)\mapsto 1$).
why it matters
This identity is the axis-total field of the gauge Lie completion certificate: the structured record that packages factor count, axis counts, axis total, Lie ranks, and Lie-rank sum as one checked object. It is the numerical hinge of the cube-to-compact-factor bridge in the foundation layer (punchlist P0-S2-01): the forced $B_3$ recognition axes total six, matching the six faces of the $3$-cube forced when spatial dimension is three (forcing-chain landmark T8).
Downstream consumers of the certificate can treat "axis budget equals cube faces" as a proved equality rather than a comment. The module is explicit that this is not yet hypercharge normalization or fermion representations; it only locks the $(3,2,1)$ recognition-axis skeleton to $\mathrm{SU}(3)\times\mathrm{SU}(2)\times\mathrm{U}(1)$ and keeps Lie rank $(2,1,1)$ on a separate ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.