totalRank
The theorem establishes that the ranks of SU(3), SU(2), and U(1) in the Standard Model gauge group sum to six. Physicists deriving the SM structure from Recognition Science would cite it to confirm the (3,2,1) decomposition matches the expected total. The proof is a one-line decision procedure that evaluates the three constant definitions directly.
claim$rank(SU(3)) + rank(SU(2)) + rank(U(1)) = 6$
background
The Standard Model Group Structure module takes the gauge group as SU(3) × SU(2) × U(1) and defines the ranks as constants: rankSU3 = 3, rankSU2 = 2, rankU1 = 1. This matches the RS setting in which SU(3) rank equals spatial dimension D, SU(2) rank equals D-1, and U(1) supplies the scalar phase rank 1, for a total of 6. The module documentation states that this decomposition certifies the group-rank match with the SM and notes the five gauge boson types equal configDim D = 5.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the arithmetic equality of the three constant natural numbers.
why it matters in Recognition Science
This result supplies the rank_decomp field inside the smGroupCert definition, which certifies the full SM group structure together with gluon count and total carriers. It implements the rank decomposition stated in the module documentation and links directly to the T8 step of the forcing chain where D = 3 forces the SU(3) rank. The theorem closes the group-rank match required for the Recognition Science derivation of the Standard Model.
scope and limits
- Does not derive the gauge group factors from the forcing chain.
- Does not compute the number of physical gauge bosons.
- Does not address coupling unification or running.
- Does not prove that the (3,2,1) decomposition is unique.
formal statement (Lean)
34theorem totalRank : rankSU3 + rankSU2 + rankU1 = 6 := by decide
proof body
Term-mode proof.
35
36/-- gluon count = N² - 1 = 3² - 1 = 8 for SU(3). -/