Foundation Smgauge Algebra Weak Gen Count

The weak force's three generators

The weak nuclear force, responsible for radioactive beta decay, is not carried by a single particle but by three: the W boson, the Z boson, and their antiparticles, which together act as the force's messengers. In the mathematical language of particle physics, these messengers are the generators of the special unitary group SU(2). The framework's declaration weak_gen_count states that this group has exactly three generators, a fact it establishes by a direct calculation: the formula for the number of generators of SU(N) is N² - 1, and for N = 2, this gives 4 - 1 = 3.

This result is part of a larger, machine-checked library of formal theorems within Recognition Science. The framework models the standard model's gauge structure as emerging from the symmetries of a cube, and this declaration is the Lie-algebra-level confirmation for the weak force. It is a theorem in the library, meaning the calculation is verified by a computer proof assistant with no unproven assumptions. The theorem's practical content is a structural prediction: any gauge group arising from the same cube-based symmetry must have exactly three weak-force generators, and any deviation would falsify the identification.

The declaration does not claim to derive the weak force's other properties, such as the masses of the W and Z bosons or the strength of their interactions. It is solely a statement about the number of generators, a count that matches the empirical standard model. The framework's broader claim, that the cube's symmetries fully explain the standard model's gauge structure, is a separate, larger hypothesis that this particular theorem supports but does not by itself establish.

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

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

What this page does not claim

This theorem does not derive the masses or interaction strengths of the weak force bosons. This theorem does not prove that the cube's symmetries fully explain the standard model's gauge structure.

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: