rankU1
plain-language theorem explainer
The definition assigns the integer 1 to the rank of the U(1) factor in the Standard Model gauge group. It is referenced by electroweak unification certificates and SM group structures to complete the (3,2,1) rank decomposition that sums to 6. The implementation is a direct constant assignment with no computation or hypotheses.
Claim. In the Standard Model gauge group $SU(3)×SU(2)×U(1)$, the rank of the $U(1)$ factor equals 1.
background
The module certifies the Standard Model gauge group as $SU(3)×SU(2)×U(1)$ with ranks drawn from the Recognition Science derivation via GaugeGroupCube. SU(3) receives rank 3 matching spatial dimension D, SU(2) receives rank 2 matching D-1, and U(1) receives rank 1 as the scalar phase; the total is 6. The upstream definition in ElectrowealUnificationFromRS supplies the identical constant, which is then imported to define rankEW as rankSU2 plus rankU1.
proof idea
The declaration is a direct constant assignment of the natural number 1.
why it matters
It supplies the final term in the rank decomposition used by SMGroupCert (rankSU3 + rankSU2 + rankU1 = 6) and by ElectroweakCert (rankEW = rankSU2 + rankU1). The assignment matches the RS (3,2,1) split and the scalar-phase interpretation of U(1) within the T8 D=3 framework. It closes one link in the gauge-group certification chain while leaving open the derivation of the precise factors from the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.