su2Generators
plain-language theorem explainer
The definition assigns the constant 3 to the number of SU(2) generators. Researchers modeling weak interactions or isospin symmetry cite it to equate the adjoint dimension of SU(2) with spatial dimension D at D=3. The assignment is a direct constant with no computation or lemmas required.
Claim. The number of generators of the group SU(2) is three: $N_{SU(2)}=3$.
background
Recognition Science derives isospin as the SU(2) subgroup of rank D-1 whose adjoint has dimension D when D=3. The module states that isospin corresponds to the rank-2 sub-group of SU(3) and that five canonical multiplets match the configuration dimension at this D. Upstream result from WeakForceEmergence defines the same quantity with the comment 'Number of SU(2) generators' and the gloss 'W⁺, W⁻, Z⁰ (3 massive weak bosons)'.
proof idea
The declaration is a direct definition that assigns the constant 3. It functions as a one-line wrapper that aligns the group-theoretic count with the spatial dimension D from the forcing chain.
why it matters
This definition supplies the generator count required by IsospinCert to certify rank D-1, generator count D, and five multiplets. It also supports the equality theorems su2Generators_eq_D and weak_bosons_eq_generators in the same module and in WeakForceEmergence. The assignment realizes the T8 landmark that D=3 spatial dimensions fixes the size of the SU(2) adjoint representation, closing the geometric origin of the weak force symmetry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.