Pith. sign in
module module moderate

IndisputableMonolith.Foundation.SMGaugeAlgebra

show as:
view Lean formalization →

Defines generator counts for the Standard Model gauge algebra SU(3)×SU(2)×U(1). Records that su(N) has N²-1 generators, U(1) has one, and the SM total is 12. Supplies a small certificate packing the three factor counts. Anyone matching RS discrete structure to SM gauge ranks cites these constants; the module is pure definitional arithmetic with no nontrivial proof.

claimThe Lie algebra $\mathfrak{su}(N)$ has $N^2-1$ generators; $\mathfrak{u}(1)$ has $1$. The SM factors therefore contribute $8$ (strong), $3$ (weak) and $1$ (hypercharge), for a total of $12$ generators. A certificate records these three numbers and their sum.

background

Recognition Science works in a discrete, self-similar setting forced by the J-cost functional and the eight-tick octave. Matching that discrete skeleton to continuum particle physics requires the classical ranks of the SM gauge group $G_{\mathrm{SM}}=\mathrm{SU}(3)_c\times\mathrm{SU}(2)_L\times\mathrm{U}(1)_Y$.

The module introduces the elementary counting functions: generators of $\mathfrak{su}(N)$ equal $N^2-1$, generators of $\mathfrak{u}(1)$ equal $1$. Specializing gives the familiar $8+3+1=12$. An inductive type (or simple sum type) labels the three factors so that a single total-count lemma can be stated uniformly.

No analytic or representation-theoretic input is required; the arithmetic is definitional and sits upstream of any claim that identifies an RS combinatorial object with a gauge generator.

proof idea

This is a definition module. The generator-count functions are closed-form arithmetic expressions (N²-1, constant 1, and their specializations 8, 3, 1, 12). The certificate is a structure packing those three numbers together with a trivial equality proof that their sum is 12. No tactics beyond rfl or norm_num appear.

why it matters in Recognition Science

Supplies the numerical bridge between RS discrete structure and the classical SM gauge algebra. Downstream developments that equate an eight-tick or phi-ladder count with the 12 SM generators import these constants and the certificate. The module itself contains no open scaffolding; it simply freezes the textbook ranks so later uniqueness or matching theorems can cite a single named total.

scope and limits

declarations in this module (12)