rankU1
plain-language theorem explainer
The definition sets the rank of the U(1) electromagnetic gauge factor to 1. Researchers modeling electroweak unification in Recognition Science cite it to add to the SU(2) rank and obtain the total of 3. The assignment is a direct constant with no reduction steps.
Claim. The rank of the U(1) electromagnetic gauge factor is defined to be $1$.
background
The module decomposes the electroweak gauge group into an SU(2) weak sector of rank 2 and a U(1) electromagnetic sector of rank 1. Their sum produces rank 3, which the framework identifies with spatial dimension D. The definition is taken directly from the upstream Standard Model group structure module, where it is stated as the constant natural number 1.
proof idea
The declaration is a one-line definition that assigns the natural number 1.
why it matters
This supplies the U(1) term in the rank sum that downstream results equate to 3 and therefore to D. It completes the additive decomposition step inside the electroweak unification chain, where rank(EW) equals rank(SU(2)) plus rank(U(1)) and matches the T8 requirement that D equals 3. The value appears in ElectroweakCert to certify both the rank equality and the count of five observables.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.