rankSU2
plain-language theorem explainer
rankSU2 assigns the natural number 2 to the rank of the SU(2) gauge factor. Physicists reconstructing the Standard Model gauge structure from Recognition Science cite it when confirming the electroweak decomposition. The definition is a direct constant assignment requiring no lemmas or computation.
Claim. The rank of the Lie group SU(2) equals the natural number 2.
background
The module treats electroweak unification as the direct sum of the weak SU(2) sector and the electromagnetic U(1) sector. It records that the combined electroweak rank must equal three to match the spatial dimension D. The upstream definition in StandardModelGroupStructure supplies the identical constant for cross-module consistency.
proof idea
The definition is a direct constant assignment of 2 with no lemmas or tactics applied.
why it matters
This supplies the SU(2) component required by the ElectroweakCert structure, which asserts rankEW equals 3 and decomposes as rankSU2 plus rankU1. It participates in the totalRank theorem establishing the full Standard Model gauge rank equals 6. The assignment aligns with the framework requirement that electroweak rank matches D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.