Foundation Smgauge Algebra

The gauge generator count

In particle physics, the forces of the Standard Model are described by gauge theories, each with a set of force-carrying particles. The strong force has eight gluons, the weak force has three bosons, and the hypercharge force has one. These numbers are not arbitrary: they come from the mathematics of the symmetry groups SU(3), SU(2), and U(1), where the number of generators of SU(N) is N² - 1 and of U(N) is N². For N = 3, 2, and 1, this gives 8, 3, and 1, summing to twelve gauge bosons in total.

The framework called Recognition Science (RS) starts from a different premise: reality keeps a discrete record of recognition events, and the cost of recognition is forced by five plain conditions. From this, a chain of theorems derives the golden ratio, an eight-tick cycle, and the number 2³. The framework's machine-checked library of formal theorems then aims to show how the Standard Model's structure emerges from these foundations.

In Recognition Science, the foundation smgauge algebra module takes a specific step in this program. It proves, in the machine-checked library, that the generator counts for the three gauge factors are exactly 8, 3, and 1, and that the total is 12. The proof is direct: it defines the counts, computes each one, and sums them. The module also certifies that there are exactly three gauge factors, matching the cube-automorphism decomposition B₃ = (ℤ/2)³ ⋊ S₃, which the framework derives from the symmetries of a cube.

The structural prediction is precise: any RS-derived gauge group with the same cube-automorphism rank decomposition has exactly twelve generators. A deviation would falsify the gauge-group-from-cube identification. The module is tagged as a certificate, meaning it is a fully checked proof with zero axioms and zero unresolved goals, though the structural-rank certificate that connects this to the full gauge group structure is honestly tagged as STARTED, meaning that part remains open.

/-- Number of generators of `su(N)` is `N² - 1`. -/
def suGenCount (N : ℕ) : ℕ := N * N - 1

/-- Number of generators of `u(N)` is `N²`. -/
def uGenCount (N : ℕ) : ℕ := N * N

structure SMGaugeAlgebraCert where
  strong : factorGenCount .strong = 8
  weak : factorGenCount .weak = 3
  hyperY : factorGenCount .hyperY = 1
  total : smTotalGenCount = 12
  factor_count : Fintype.card SMGaugeFactor = 3

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

What this page does not claim

This module does not derive the full gauge group structure, only the generator counts. This module does not prove that the Standard Model's gauge groups are the only possible ones. This module does not derive the values of the coupling constants or any other physical parameters.

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: