compactGaugeFactor_count
plain-language theorem explainer
The compact gauge factors selected by the cube-layer completion rule form a three-element set: color SU(3), weak SU(2), and hypercharge U(1). Anyone citing the cube-to-Standard-Model gauge bridge or the gauge-Lie completion certificate needs this cardinality. The proof is a one-line decidability check on the finite inductive type.
Claim. The finite type of compact gauge factors arising from the cube-layer completion rule has cardinality $3$.
background
The module records the first clean bridge from the forced $B_3$ cube-layer skeleton to the Standard Model compact gauge factors. Prior cube work fixes recognition-axis counts $(3,2,1)$ (total $6$): three axis permutations, an even sign-flip completion of order $2$, and a parity quotient of order $1$. The compact-completion rule sends those counts to $\mathrm{SU}(3)$ color, $\mathrm{SU}(2)$ weak isospin, and $\mathrm{U}(1)$ hypercharge phase.
CompactGaugeFactor is the inductive enumeration of those three factors, deriving Fintype. The module keeps this factor list separate from Lie rank $(2,1,1)$ (total $4$). This is not yet a hypercharge or fermion-representation derivation; it is only the factor skeleton.
proof idea
One-line decidability proof. The inductive type has three constructors and derives Fintype and DecidableEq, so Fintype.card evaluates by decide to $3$. No lemmas beyond the derived instances are required.
why it matters
Supplies the factor_count field of the local gauge-Lie completion certificate, which packages factor count, recognition-axis counts/total, and Lie ranks/sum as a single certificate object. Downstream, the Unified Forcing Chain theorem t8_to_gauge_standard_model_bridge_holds routes T8 (forced $D=3$) through the cube/spinor skeleton into gauge and Standard Model surfaces; this cardinality is the discrete count of compact factors on that bridge.
In framework terms it is the first step of punchlist item P0-S2-01: cube layer counts map onto the familiar $\mathrm{SU}(3)\times\mathrm{SU}(2)\times\mathrm{U}(1)$ factor list. It does not yet close hypercharge normalization or fermion reps; those remain later bridge obligations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.