wBosonCount
plain-language theorem explainer
The definition computes the W boson count as the square of the SU(2) rank minus one. Researchers reconstructing the Standard Model gauge boson spectrum in Recognition Science cite it when assembling the pre-EWSB carrier total. It is realized as a direct arithmetic expression on the fixed rank value.
Claim. The W-boson multiplicity equals $r^2 - 1$ where $r = 2$ is the rank of the SU(2) factor.
background
The module certifies the Standard Model gauge group SU(3)×SU(2)×U(1) via rank decomposition from Recognition Science, with ranks 3, 2, 1 summing to 6 and matching spatial dimension D for SU(3). The rankSU2 definition, appearing in both ElectroweakUnificationFromRS and this module, fixes the value at 2. This supplies the W contribution among the five gauge boson types that equal configDim D = 5.
proof idea
The declaration is a one-line definition that squares the rankSU2 constant and subtracts one.
why it matters
It supplies the numerical term 3 inside totalCarriers, which sums gluonCount + wBosonCount + rankU1 to obtain 12 carriers before EWSB. The definition completes the SU(2) sector of the RS-derived group structure, consistent with the eight-tick octave and D = 3. The downstream theorem w_boson_count immediately certifies the value 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.