Foundation Smgauge Algebra Smgauge Algebra Cert

The gauge certificate

In particle physics, the Standard Model describes three of the four fundamental forces through gauge theories. Each force has a symmetry group, and each group has a number of generators, the basic building blocks of its transformations. The strong force uses SU(3) with 8 generators, the weak force uses SU(2) with 3, and the hypercharge force uses U(1) with 1. These counts are not arbitrary: for the special unitary groups, the number of generators of SU(N) is N² − 1, giving 8 for N=3 and 3 for N=2, while U(1) has 1 generator. Adding them gives 12 total gauge generators, a standard and well-known fact in the Standard Model.

The Recognition Science framework's machine-checked library of formal theorems contains a declaration called SMGaugeAlgebraCert. This is a certificate, a formal object that bundles together the generator counts as proved facts. The certificate records four theorems: the strong factor has 8 generators, the weak factor has 3, the hypercharge factor has 1, and the total is 12. It also records that there are exactly three gauge factors. Each of these statements is proved by direct computation in the framework's library, with no gaps or unproved assumptions. The certificate itself is a structure that packages these five facts into a single object, and the library provides a proof that such a certificate exists.

In Recognition Science, this certificate connects to a larger claim. The framework derives the Standard Model's gauge group structure from the symmetries of a cube. A separate result proves that the rank decomposition of the cube's automorphism group matches the Standard Model gauge group ranks (3, 2, 1). This certificate adds the Lie-algebra-level detail: the generator counts (8, 3, 1) match the dimensions (N²−1, N²−1, 1) for N=3, 2, 1. The structural prediction is that any gauge group derived from the same cube-automorphism rank decomposition has exactly 12 generators. A deviation from this count would falsify the identification of the gauge group with the cube's symmetries.

What the certificate does not claim is important. It does not prove that the Standard Model's gauge group is the only possible one, nor does it derive the actual values of the coupling constants or any particle masses. The certificate merely establishes the generator counts as formal theorems. The connection from cube symmetries to the Standard Model gauge group is a separate identification, and the full structural-rank certificate is honestly tagged as STARTED, meaning it is not yet complete. The generator counts are solid, but the bridge from cube to gauge group is a work in progress.

theorem strong_gen_count : factorGenCount .strong = 8 := by decide

theorem weak_gen_count : factorGenCount .weak = 3 := by decide

theorem hyper_gen_count : factorGenCount .hyperY = 1 := by decide

theorem sm_total_gen_count : smTotalGenCount = 12 := by decide

/-- Number of SM gauge factors = 3, matching the cube-automorphism
three-layer decomposition. -/
theorem factor_count : Fintype.card SMGaugeFactor = 3 := by decide

/-- SM gauge-algebra certificate. -/
def smGaugeAlgebraCert : SMGaugeAlgebraCert where
  strong := strong_gen_count
  weak := weak_gen_count
  hyperY := hyper_gen_count
  total := sm_total_gen_count
  factor_count := factor_count

What this page does not claim

The certificate does not prove that the Standard Model gauge group is unique. The certificate does not derive coupling constants, particle masses, or any dynamics. The full structural-rank certificate connecting cube symmetries to gauge groups is not yet complete.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/SMGaugeAlgebra.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: