pith. machine review for the scientific record. sign in
def definition def or abbrev high

totalCarriers

show as:
view Lean formalization →

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.

claimThe 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  45def totalCarriers : ℕ := gluonCount + wBosonCount + rankU1

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (5)

Lean names referenced from this declaration's body.