rankEW
plain-language theorem explainer
The definition assigns the electroweak rank as the arithmetic sum of the SU(2) rank and U(1) rank, producing the natural number 3. Physicists deriving Standard Model structure from Recognition Science cite this when equating the electroweak group dimension to the forced spatial dimension D. The definition is a direct one-line sum of two constant natural-number definitions.
Claim. Let $r_{EW}$ denote the rank of the electroweak group $SU(2)×U(1)$. Then $r_{EW} := r_{SU(2)} + r_{U(1)}$, where $r_{SU(2)}=2$ and $r_{U(1)}=1$.
background
In the Recognition Science module on electroweak unification the electromagnetic sector is identified with the U(1) factor of rank 1 and the weak sector with the SU(2) factor of rank 2. Their direct product therefore carries rank equal to the sum of these two integers, and the module states that this sum equals the spatial dimension D forced by the eight-tick octave. The upstream definitions in both the local module and the Standard Model group structure module fix rankSU2 as the constant 2 and rankU1 as the constant 1.
proof idea
This declaration is a one-line definition that directly computes the sum of the two upstream rank constants rankSU2 and rankU1.
why it matters
The definition supplies the rank value required by the ElectroweakCert structure and by the theorems rankEW_eq_D and ew_from_su2_u1. It completes the structural step that identifies the electroweak rank with D=3, consistent with the forcing-chain result T8 that spatial dimensions equal 3. The parent theorems both rely on this sum to certify unification at the level of group rank.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.