ew_from_su2_u1
plain-language theorem explainer
The theorem asserts that the electroweak group rank equals the sum of the SU(2) and U(1) ranks. Recognition Science modelers cite it when confirming that the total rank matches the spatial dimension D in the Standard Model derivation. The proof reduces to a single reflexivity step that follows immediately from the definition of the electroweak rank as that sum.
Claim. $rank(EW) = rank(SU(2)) + rank(U(1))$
background
The Electroweak Unification from RS module treats the electroweak group as the product SU(2) × U(1) inside the Recognition Science framework. The SU(2) rank is defined as 2 and the U(1) rank as 1, so their sum defines the electroweak rank. This implements the structural claim that the electroweak rank equals D = 3 from the forcing chain T8.
proof idea
The proof is a one-line wrapper that applies reflexivity to the definition of the electroweak rank as the sum of the SU(2) and U(1) ranks. No further lemmas or tactics are required.
why it matters
It supplies the rank_sum field inside the electrowealCert structure, which also records the rank-D equality and the count of five observables. The result closes the group-rank step in the RS electroweak unification before the J-cost threshold is imposed at the unification scale, consistent with T8 where D equals 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.