electrowealCert
plain-language theorem explainer
ElectroweakCert is instantiated by supplying the rank equality to three, the count of five observables, and the additive decomposition of ranks from SU(2) and U(1). A researcher deriving the Standard Model gauge structure from Recognition Science symmetries would cite this when confirming that the electroweak sector saturates the spatial dimension count. The definition is assembled directly from three prior results that establish each field by decision or reflexivity.
Claim. Let $r_{EW}$ denote the rank of the electroweak group, $r_{SU(2)}$ the rank of SU(2), and $r_{U(1)}$ the rank of U(1). The electroweak certification asserts $r_{EW}=3$, that the number of electroweak observables is five, and that $r_{EW}=r_{SU(2)}+r_{U(1)}$.
background
Recognition Science derives the electroweak unification by matching the combined rank of SU(2) × U(1) to the spatial dimension D = 3. The structure ElectroweakCert packages three assertions: the rank equality to D, the cardinality of the set of five canonical observables (W⁺, W⁻, Z, photon, and the Weinberg angle), and the rank sum identity. The local setting is the module on electroweak unification from RS, which treats the unification scale as the point where the J-cost of the split field equals the canonical threshold. Upstream, rankEW_eq_D establishes rankEW = 3 by decision, ewObservableCount shows the observable count is five by decision, and ew_from_su2_u1 gives the rank decomposition by reflexivity. A related result from CubicSymmetryGroupFromRS shows a rank decomposition sum of six.
proof idea
This definition constructs the ElectroweakCert structure by direct assignment of its three fields. The ew_rank_D field is filled by the theorem rankEW_eq_D, the five_observables field by ewObservableCount, and the rank_sum field by ew_from_su2_u1. No further reasoning is required beyond these prior results.
why it matters
This definition supplies the certified object for the electroweak sector in the Recognition Science framework, confirming that the gauge rank sums to the spatial dimension D = 3 and that five observables match the configuration dimension. It realizes the structural claim in the module documentation that rank(EW) = rank(SU(2)) + rank(U(1)) = 3 = D. The result closes the electroweak unification step by providing a concrete instance without axioms or sorrys.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.