w_boson_count
plain-language theorem explainer
The declaration certifies that the W-boson multiplicity equals three inside the SU(2) factor of the gauge group. Particle physicists reconstructing the Standard Model from Recognition Science cite the count when enumerating the twelve pre-EWSB force carriers. The proof reduces to a single decision procedure on the closed arithmetic expression for the adjoint dimension.
Claim. The W-boson count equals three, where this count is defined by the formula $r^2 - 1$ evaluated at the rank $r = 2$ of the SU(2) factor.
background
The module certifies that the Standard Model gauge group SU(3) × SU(2) × U(1) arises from the Recognition Science gauge-group cube, producing the rank triple (3, 2, 1). The W-boson count is the adjoint dimension of SU(2), given explicitly by the expression rank squared minus one. The upstream definition of temporal ordering states that snapshot A precedes snapshot B precisely when the tick index of A is strictly smaller than that of B.
proof idea
The proof is a one-line wrapper that invokes the decide tactic on the decidable equality between the natural-number value of the W-boson count and the numeral three.
why it matters
The equality supplies the middle term in the pre-EWSB carrier total of twelve (eight gluons plus three W bosons plus one remaining), supporting the module's verification that the observed rank decomposition matches the Standard Model. It sits inside the broader Recognition Science derivation of gauge structure from the forcing chain and the three-dimensional spatial emergence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.