ewObservableCount
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not compute numerical masses or couplings of the observables.
- Does not derive the J-cost equality at the unification threshold.
- Does not address the strong-force sector or full Standard Model embedding.
- Does not prove stability of the five-observable count under renormalization.
Lean usage
example : Fintype.card EWObservable = 5 := ewObservableCountformal statement (Lean)
36theorem ewObservableCount : Fintype.card EWObservable = 5 := by decide
proof body
37