CompactGaugeFactor
plain-language theorem explainer
Names the three compact gauge factors forced by the 3-cube completion rule: SU(3), SU(2), and U(1). Anyone citing the cube-to-Standard-Model gauge skeleton uses this finite enumeration as the carrier type for axis counts, Lie ranks, and boson multiplicities. The declaration is a plain inductive with decidable equality and a finite-type instance; no proof content.
Claim. There is a finite set of compact gauge factors selected by the cube-layer completion rule, with three elements corresponding to $\mathrm{SU}(3)$ (color), $\mathrm{SU}(2)$ (weak isospin), and $\mathrm{U}(1)$ (hypercharge phase).
background
The module records the first bridge from the forced $B_3$ cube layer to the Standard Model compact gauge skeleton. Prior cube work already fixes three recognition-axis counts: axis permutations equal $3$, even sign-flip completion equal $2$, and the parity quotient equal $1$. The completion rule maps those counts onto compact factors by $3\mapsto\mathrm{SU}(3)$, $2\mapsto\mathrm{SU}(2)$, $1\mapsto\mathrm{U}(1)$.
Two numerical notions are kept deliberately separate. Recognition-axis count is the triple $(3,2,1)$ with total $6$; Lie rank is $(2,1,1)$ with total $4$. This inductive type is only the discrete label set for those assignments. It is not yet a derivation of hypercharge normalizations or fermion representations.
In the broader forcing chain, spatial dimension $D=3$ (T8) supplies the cube whose skeleton this factor set completes.
proof idea
No proof: the declaration is an inductive type with three nullary constructors (color, weak, hypercharge phase), deriving decidable equality, a printable representation, Boolean equality, and a Fintype instance so that the factor set is finite and enumerable by decide.
why it matters
This is the discrete carrier for every numeric assignment in the gauge-Lie completion module: recognition-axis count $(3,2,1)$, Lie rank $(2,1,1)$, and adjoint/phase carrier counts $(8,3,1)$. Downstream certificates package the factor count and axis assignments into GaugeLieCompletionCert, and the same labels feed the T8-to-gauge Standard Model bridge in the unified forcing chain (the cube dimension forced by T8 supplies this skeleton).
It closes the first clean step of punchlist item P0-S2-01: cube layer counts to compact gauge-factor skeleton. Full hypercharge embedding and fermion representations remain open; this only freezes the three-factor menu.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.