totalCarriers
plain-language theorem explainer
The definition computes the total number of gauge bosons in the unbroken Standard Model as the sum of eight gluons from SU(3), three from SU(2), and one from U(1). Gauge theorists reconstructing the SM spectrum from Recognition Science would cite the count when verifying the pre-EWSB boson inventory. It is realized as a direct arithmetic sum of the three group contributions.
Claim. The total number of force carriers is defined by $n = 8 + 3 + 1$, where the summands are the adjoint dimension of SU(3), the adjoint dimension of SU(2), and the rank of U(1).
background
The module reconstructs the Standard Model gauge group SU(3) × SU(2) × U(1) from Recognition Science by matching ranks to spatial dimensions: SU(3) rank equals D = 3, SU(2) rank equals D - 1 = 2, and U(1) supplies the scalar phase of rank 1. Gluon count is the adjoint dimension rank(SU(3))² - 1 = 8; W-boson count is rank(SU(2))² - 1 = 3; the U(1) term is its rank 1. Upstream definitions supply these values independently: gluonCount from rankSU3² - 1, wBosonCount from rankSU2² - 1, and rankU1 fixed at 1. The local setting notes that five boson types equal configDim D = 5 while the carrier count reaches 12 and the group rank sums to 6.
proof idea
The definition is a one-line arithmetic sum of the gluon count, W-boson count, and U(1) rank supplied by the sibling definitions.
why it matters
This definition supplies the total carrier count referenced by the SMGroupCert structure (certifying five types, rank sum 6, gluon count 8, and total 12) and by the total_carriers_eq theorem (proving equality to 12). It completes the force-carrier enumeration step in the RS reconstruction of the Standard Model group structure, consistent with the T8 assignment of D = 3 and the GaugeGroupCube construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.