rankEW_eq_D
plain-language theorem explainer
rankEW_eq_D shows that the electroweak gauge group rank equals three spatial dimensions. Unification modelers in the Recognition Science setting cite this when identifying SU(2)×U(1) structure with forced dimensionality. The proof is a one-line decision procedure that confirms the sum after the additive definition unfolds.
Claim. The rank of the electroweak group, defined as the sum of the SU(2) rank and the U(1) rank, equals the spatial dimension $D = 3$.
background
The module decomposes electroweak unification into SU(2) weak and U(1) electromagnetic sectors whose ranks add. rankEW is introduced as the direct sum rankSU2 + rankU1, with the module stating that this total equals D. The local setting identifies five canonical observables (W⁺, W⁻, Z, γ, mixing angle) with configDim D = 5 and treats the rank equality as the structural link to spatial dimensionality.
proof idea
The proof is a one-line wrapper that applies the decide tactic. Once rankEW expands to the sum of the sibling integer definitions rankSU2 = 2 and rankU1 = 1, the decision procedure verifies equality to 3 with no further steps.
why it matters
This theorem supplies the ew_rank_D field inside the ElectroweakCert record. It realizes the module claim that rank(EW) = rank(SU(2)) + rank(U(1)) = 3 = D. In the Recognition Science framework it instantiates the T8 step that forces D = 3 through group-rank addition, anchoring the electroweak sector to the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.