su2Generators_eq_D
plain-language theorem explainer
The declaration establishes that the number of SU(2) generators equals three. Researchers deriving isospin symmetry from Recognition Science would cite this when matching the adjoint dimension to the three spatial dimensions. The proof is a one-line reflexivity from the constant definition of the generator count.
Claim. The adjoint representation of the SU(2) group has dimension three: $3$.
background
The module identifies isospin symmetry with the SU(2) group relating proton and neutron states. In Recognition Science this appears as the rank-2 subgroup of SU(3) once the spatial dimension reaches D=3. The module doc records that the generator count equals D while the rank equals D-1, and that five canonical multiplets match the configuration dimension at D=5.
proof idea
The proof is a one-line wrapper that applies reflexivity to the definition of the generator count, which is fixed at the constant 3.
why it matters
This equality is invoked inside the isospinCert construction to complete the isospin certificate. It realizes the T8 step of the forcing chain by setting the generator count to D=3, supporting the three massive weak bosons and the five isospin multiplets.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.