total_carriers_eq
plain-language theorem explainer
The theorem states that the total number of force carriers before electroweak symmetry breaking equals 12. A physicist deriving the Standard Model gauge structure inside Recognition Science would cite it to close the carrier count that matches the rank decomposition. The proof is a one-line decision procedure that evaluates the arithmetic definition of totalCarriers directly.
Claim. The total number of gauge bosons before electroweak symmetry breaking satisfies $N = 12$, where $N$ is defined as the sum of the gluon count, the W-boson count, and the U(1) rank.
background
The module derives the Standard Model gauge group SU(3) × SU(2) × U(1) from the Recognition Science rank decomposition (3,2,1) that aligns with spatial dimension D = 3. The upstream definition totalCarriers is given explicitly as gluonCount + wBosonCount + rankU1 and is described as the total force carriers: 8 + 3 + 1 = 12 before EWSB. This count is independent of the five gauge-boson types that equal configDim D = 5.
proof idea
The proof is a one-line wrapper that applies the decide tactic to evaluate the natural-number arithmetic inside the definition of totalCarriers.
why it matters
The equality supplies the total_12 field inside the smGroupCert structure that certifies the full group-rank match for the Standard Model. It closes the carrier accounting consistent with the eight-tick octave and D = 3 forcing the SU(3) rank while leaving the post-EWSB spectrum for later modules. No open scaffolding remains in this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.