pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Foundation.SMGaugeAlgebra

show as:
view Lean formalization →

The SMGaugeAlgebra module supplies generator counts for the Standard Model gauge groups inside the Recognition Science foundation. It states that su(N) has N squared minus one generators and extends the count to U(1) and the full SM factor. Researchers assembling gauge degrees of freedom for mass formulas or interaction counts cite these values. The module contains only definitions and no proof obligations.

claimThe Lie algebra of the special unitary group satisfies $dim(su(N)) = N^2 - 1$.

background

This module sits in the Foundation layer and introduces the generator-counting functions for the Standard Model gauge algebra. It defines suGenCount(N) as the dimension of su(N), uGenCount for the U(1) factor, and SMGaugeFactor together with the combined smTotalGenCount. The setting imports basic Lie-algebra facts from Mathlib and applies them to the groups SU(3), SU(2), and U(1) that appear in the SM gauge structure.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The generator counts supplied here are prerequisites for the SM gauge algebra certification and total generator tally used in downstream particle-mass and interaction calculations. They furnish the algebraic degrees of freedom that enter the Recognition Science treatment of gauge bosons on the phi-ladder.

scope and limits

declarations in this module (12)