carrierCount
plain-language theorem explainer
Assigns each compact gauge factor its adjoint/phase carrier count: 8 for SU(3), 3 for SU(2), 1 for U(1). Cited wherever the cube-to-SM gauge skeleton needs boson multiplicities before electroweak mixing. Implemented as a three-clause pattern match on the factor constructors.
Claim. The gauge-boson carrier count on compact factors is $n^2-1$ for $\mathrm{SU}(n)$ and $1$ for $\mathrm{U}(1)$: $\mathrm{SU}(3)\mapsto 8$, $\mathrm{SU}(2)\mapsto 3$, $\mathrm{U}(1)\mapsto 1$.
background
The module records the first bridge from the forced $B_3$ cube-layer skeleton to the Standard Model compact gauge factors. Cube work already forces recognition-axis counts $(3,2,1)$ (axis permutations, even sign-flip completion, parity quotient). The completion rule sends those to $\mathrm{SU}(3)$, $\mathrm{SU}(2)$, and $\mathrm{U}(1)$ respectively.
CompactGaugeFactor is the three-constructor inductive type for those factors. Two tallies are kept separate: recognition-axis count $(3,2,1)$ totaling 6, and Lie rank $(2,1,1)$ totaling 4. Carrier count is the third tally: adjoint (or phase) dimension of each factor, i.e. the number of gauge bosons before electroweak mixing.
This is not yet hypercharge embedding or fermion representations; it is only the compact-factor skeleton and its numerical bookkeeping.
proof idea
Definition by exhaustive cases on CompactGaugeFactor. The $\mathrm{SU}(3)$ and $\mathrm{SU}(2)$ arms are the standard adjoint dimensions $n^2-1$; the $\mathrm{U}(1)$ arm is the single phase generator. No lemmas are invoked; evaluation is pure computation on the constructors.
why it matters
Supplies the boson multiplicities that carrier_counts and carrier_total decide: $8$, $3$, $1$ and sum $12$ before electroweak mixing. Those facts feed GaugeLieCompletionCert, the local certificate that the cube completion yields three compact factors with the expected axis counts.
Downstream, T8_To_GaugeStandardModel_Bridge in the unified forcing chain routes T8 (forced $D=3$) into the gauge/SM skeleton; carrier bookkeeping is part of that bridge's numerical spine. In the Recognition framework this is the first clean numerical link from the eight-tick / three-cube layer counts to the SM gauge-boson census, without yet claiming hypercharge or fermion content.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.