ElectroweakCert
plain-language theorem explainer
ElectroweakCert packages three facts that certify the electroweak sector in Recognition Science: its rank equals the spatial dimension 3, it contains exactly five observables, and the rank decomposes additively from SU(2) and U(1). A physicist verifying RS-derived group structures or unification at the phi-ladder scale would cite this certificate to confirm consistency with cubic symmetry. The structure is assembled directly from three decidable equalities supplied by sibling definitions and the Fintype instance on EWObservable.
Claim. A structure asserting that the electroweak rank equals 3, that the set of electroweak observables (W⁺, W⁻, Z, photon, mixing angle) has cardinality 5, and that the electroweak rank equals the sum of the SU(2) rank 2 and the U(1) rank 1.
background
In the Recognition Science module on electroweak unification, the electroweak group is realized as SU(2) × U(1) whose ranks add to three, matching the spatial dimension D fixed by the eight-tick octave. The inductive type EWObservable enumerates the five canonical observables W⁺, W⁻, Z, photon and mixingAngle, equipped with a derived Fintype instance. Upstream definitions set rankSU2 := 2, rankU1 := 1 and rankEW := rankSU2 + rankU1, while the rank_sum theorem from CubicSymmetryGroupFromRS records a related decomposition that sums to six.
proof idea
The declaration is a plain structure definition with no proof body. Its three fields are populated by direct reference to the sibling definitions rankEW, rankSU2, rankU1 and the Fintype instance on the five-constructor inductive EWObservable; each equality is discharged by decide in the downstream wrapper electrowealCert.
why it matters
ElectroweakCert supplies the bundled certificate consumed by electrowealCert, which verifies that the electroweak sector matches the three-dimensional spatial lattice required by Recognition Science. It encodes the module claim that rank(EW) = rank(SU(2)) + rank(U(1)) = 3 = D, closing the unification step in the A1 SM Depth section and linking the five observables to the J-cost threshold and phi-ladder. No open scaffolding remains in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.