rankSU2
plain-language theorem explainer
The declaration sets the rank of SU(2) to the integer 2 inside the RS-derived decomposition of the Standard Model gauge group. Model builders checking the (3,2,1) rank match against observed forces would cite this constant when assembling the total rank or electroweak substructure. The assignment is a direct constant definition with no further reduction.
Claim. The rank of the Lie group SU(2) equals 2.
background
The module treats the Standard Model gauge group as SU(3) × SU(2) × U(1) and records its rank decomposition as 3 + 2 + 1 = 6. SU(3) rank is identified with spatial dimension D, SU(2) rank with D - 1, and U(1) rank with the residual phase. The upstream definition in ElectrowealUnificationFromRS supplies the identical constant value 2 for rankSU2.
proof idea
Direct definition that binds the natural number 2 to the identifier rankSU2. No lemmas or tactics are invoked; the body is a literal constant assignment.
why it matters
The constant enters SMGroupCert to certify the five boson types and the rank sum of 6, and it is added inside rankEW and the ew_from_su2_u1 theorem. It supplies the middle term of the (3,2,1) decomposition required by the RS forcing chain once D = 3 is fixed at T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.