rankU1
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.
claimIn 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 in Recognition Science
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.
scope and limits
- Does not derive the U(1) rank from the Recognition functional equation or J-cost.
- Does not enumerate gauge bosons or compute multiplicities such as gluonCount.
- Does not address electroweak symmetry breaking or observable counts.
- Does not constrain the full Lie-algebra structure beyond the rank integer.
formal statement (Lean)
32def rankU1 : ℕ := 1
proof body
Definition body.
33