pith. sign in
module module high

IndisputableMonolith.Foundation.SMGaugeAlgebra

show as:
view Lean formalization →

The SMGaugeAlgebra module supplies the generator counts for the su(N) Lie algebras appearing in the Standard Model gauge group. Researchers assembling the algebraic structure of the SM in Recognition Science would cite these counts when computing total gauge dimensions. The module consists of definitions implementing the standard formula dim(su(N)) = N² - 1 for the strong, weak, and hypercharge factors.

claimThe dimension of the Lie algebra su(N) is given by dim(su(N)) = N² - 1.

background

This module resides in the Foundation layer and imports only Mathlib. It introduces counting functions such as suGenCount, uGenCount, factorGenCount, and the composite smTotalGenCount that implement the classical dimension formula for the special unitary algebras. The central identity supplied by the module is the standard result that su(N) possesses N² - 1 generators. These counts later combine to give the total number of gauge generators in the Standard Model.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The generator counts defined here feed smTotalGenCount and SMGaugeAlgebraCert. They supply the numerical input required for any later statement about the dimension of the full SM gauge algebra within the Recognition Science framework.

scope and limits

declarations in this module (12)