EWObservable
plain-language theorem explainer
EWObservable enumerates the five canonical electroweak observables required by RS unification: the charged weak bosons W+ and W-, the neutral boson Z, the photon, and the weak mixing angle. A physicist deriving the electroweak sector from the Recognition Science forcing chain cites this to match observable count to spatial dimension D. The declaration is a direct inductive type equipped with Fintype, Repr, and decidable equality, enabling immediate cardinality verification by decision procedure.
Claim. Let $O_{EW}$ be the finite set of electroweak observables defined by the constructors $W^+$, $W^-$, $Z$, photon, and mixing angle, where mixing angle is the sine of half the generational phase difference.
background
The module shows electroweak unification from RS by equating the combined rank of SU(2) and U(1) to the spatial dimension D=3. The upstream anchor map Z assigns integer values to lepton, up-quark, and down-quark sectors via quadratic and quartic powers of scaled charge. The mixing angle is the sine of half the phase difference between generations, with the largest value between the first and second generations.
proof idea
The declaration is an inductive definition that lists the five observables explicitly and derives Fintype, Repr, BEq, and DecidableEq instances in one step.
why it matters
This definition supplies the type for ElectroweakCert, which certifies rankEW equals 3, observable cardinality equals 5, and rank sum equals rankSU2 plus rankU1. It implements the module claim that five canonical EW observables equal configDim D=5 and closes the link from the RS rank sum to T8 spatial dimension D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.