su2Generators
plain-language theorem explainer
The definition sets the number of SU(2) generators to three to match the three spatial dimensions from which the weak force emerges in Recognition Science. Electroweak unification researchers would cite it when connecting gauge structure to ledger geometry. It is introduced by direct assignment equating the count to the three massive weak bosons.
Claim. The number of generators of the SU(2) group is $3$.
background
The Weak Force Emergence module shows how the weak nuclear force arises from ledger geometry in Recognition Science. The SU(2)_L symmetry is identified with the three generators of rotations in three spatial dimensions, as stated in the module: the weak force is mediated by W⁺, W⁻, and Z⁰ bosons emerging from 3D ledger geometry. Upstream results define W as the wallpaper group count in related modules on masses and topology, but the generator count here is fixed independently at three to align with the spatial dimension landmark.
proof idea
The definition is a direct constant assignment of the value 3. It requires no lemmas or tactics beyond the identification of the three weak bosons with the three rotation generators.
why it matters
This definition supplies the generator count used in the IsospinCert structure and in the theorems su2_from_3d and weak_bosons_eq_generators that equate generators to weak boson count. It realizes the framework step T8 that fixes D = 3 spatial dimensions and thereby forces the SU(2) structure for the weak force, as described in the module's RS Mechanism section on gauge symmetry from 3D geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.