ewObservableCount
plain-language theorem explainer
The declaration asserts that the electroweak sector contains exactly five canonical observables. Physicists constructing unification models from Recognition Science would cite this count to confirm the structural match with configuration dimension. The proof is a direct computation that enumerates the five constructors of the defining inductive type.
Claim. The finite set of electroweak observables, consisting of the positive W boson, negative W boson, Z boson, photon, and mixing angle, has cardinality five: $|EWObservable| = 5$.
background
The Electroweak Unification from RS module constructs the electroweak sector as SU(2) × U(1) with total rank three, matching the spatial dimension D from the forcing chain. The EWObservable inductive type enumerates the five canonical observables required at the unification scale where J-cost of the split field equals the canonical threshold. This count is stated to equal configDim D = 5 in the module documentation.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the Fintype.card computation on EWObservable, which derives Fintype, DecidableEq, and Repr from its five constructors.
why it matters
This supplies the five_observables field inside the ElectroweakCert definition, completing the structural certification that rank(EW) = D together with the rank sum from SU(2) and U(1). It directly instantiates the T8 step fixing D = 3 and the rank-addition rule rank(EW) = rank(SU(2)) + rank(U(1)) = 3. The module documentation ties the result to the ~100 GeV unification scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.