su2Rank
plain-language theorem explainer
The definition assigns the natural number 2 to the rank of the SU(2) isospin symmetry group. Researchers deriving isospin from Recognition Science would reference this value when linking the group rank to the spatial dimension minus one at D equals 3. The assignment is immediate with no proof obligations or reductions involved.
Claim. The rank of the SU(2) isospin group is defined to be $2$.
background
In the module on isospin symmetry derived from Recognition Science, isospin is identified with the SU(2) symmetry relating the proton and neutron. This corresponds to the rank-2 subgroup of SU(3) in the RS framework. The key identification is that the SU(2) rank equals D minus 1, where D is the spatial dimension fixed at 3 by the forcing chain.
proof idea
The definition is a direct constant assignment of 2 to the rank. No lemmas or tactics are applied; the value is hardcoded to align with the dimension D equals 3.
why it matters
This definition supplies the numerical value for the SU(2) rank that is required by the IsospinCert structure and the equality theorem su2Rank_eq_Dm1. It fills the step in the Recognition Science chain where the isospin group rank is set to D minus 1, consistent with T8 fixing three spatial dimensions. The module establishes the correspondence between isospin multiplets and the configuration dimension of 5.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.