IndisputableMonolith.Physics.StandardModelGroupStructure
Defines the Standard Model gauge algebra ranks and carrier counts: SU(3), SU(2), U(1) with total rank 4, eight gluons, three weak bosons, and twelve gauge carriers. Physicists matching RS forcing output to SM quantum numbers cite these constants. The module is mostly definitional equalities and closed arithmetic facts.
claimThe SM gauge group is $SU(3)\times SU(2)\times U(1)$ with ranks $r_{SU(3)}=2$, $r_{SU(2)}=1$, $r_{U(1)}=1$, total rank $4$. Gluon count is $N^2-1=8$ for $SU(3)$; $W$ bosons number $3$; total gauge carriers equal $12$.
background
Recognition Science aims to force the observed gauge structure rather than postulate it. In the SM the color factor is $SU(3)$ (rank 2, adjoint dimension $8$), the weak factor is $SU(2)$ (rank 1, three $W$ bosons), and hypercharge is $U(1)$ (rank 1). The total rank is therefore $2+1+1=4$, and the total number of gauge bosons (carriers) is $8+3+1=12$.
This module packages those classical Lie-algebra facts as named Lean constants and equalities so downstream RS physics lemmas can refer to them without re-deriving $N^2-1$ or the rank sum. The only import is Mathlib; no RS-specific cost functional appears here.
proof idea
Definition module with thin arithmetic wrappers. Ranks and boson counts are introduced as numerals or simple closed forms (e.g. gluon count as $3^2-1$). Equalities such as total carriers and the gluon-count identity are discharged by norm_num or rfl-style evaluation. No nontrivial tactic proof or external lemma chain.
why it matters in Recognition Science
Supplies the SM-side integers that any RS derivation of gauge structure must hit: eight gluons, three weak bosons, total rank four, twelve carriers. Downstream physics modules that connect the eight-tick octave (T7), $D=3$ (T8), or the forced internal symmetry pattern to the observed SM use these names as the target values. Without a single place for rank and adjoint dimensions, matching lemmas would scatter magic numbers. The module itself does not force the group; it only records the classical target.
scope and limits
- Does not derive SU(3)×SU(2)×U(1) from the RS forcing chain.
- Does not treat fermion representations, hypercharge assignments, or anomaly cancellation.
- Does not include the Higgs sector or spontaneous symmetry breaking.
- Does not prove uniqueness of these ranks inside RS; only records SM values.