totalCarriers
plain-language theorem explainer
The definition sums the gluon count from SU(3), the W-boson count from SU(2), and the U(1) rank to obtain the total of 12 force carriers before electroweak symmetry breaking. Researchers matching Recognition Science derivations to Standard Model gauge structure would cite this count when verifying the (3,2,1) rank decomposition. It is a direct arithmetic definition combining three sibling counts.
Claim. The total number of force carriers is $N = N_g + N_W + r_{U(1)}$ where $N_g = 8$ is the gluon count from SU(3), $N_W = 3$ is the W-boson count from SU(2), and $r_{U(1)} = 1$.
background
The module derives the Standard Model gauge group SU(3)×SU(2)×U(1) from the Recognition Science rank decomposition (3,2,1) tied to spatial dimension D=3. GluonCount is defined as rankSU3² - 1 = 8, wBosonCount as rankSU2² - 1 = 3, and rankU1 as 1. The module doc states that five gauge boson types equal configDim D=5 while the carrier total before EWSB is 12.
proof idea
This is a direct definition that adds the three component counts gluonCount, wBosonCount, and rankU1.
why it matters
The definition supplies the total carrier count asserted in SMGroupCert via the field total_12 : totalCarriers = 12, which is discharged by the theorem total_carriers_eq. It completes the gauge-boson counting step in the RS derivation of the SM group structure from the (3,2,1) ranks. The framework landmark is the match between rank decomposition and observed carrier multiplicity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.