  33  | Wplus | Wminus | Z | photon | mixingAngle
  34  deriving DecidableEq, Repr, BEq, Fintype
  35
  36theorem ewObservableCount : Fintype.card EWObservable = 5 := by decide
  37
  38structure ElectroweakCert where
  39  ew_rank_D : rankEW = 3
  40  five_observables : Fintype.card EWObservable = 5
  41  rank_sum : rankEW = rankSU2 + rankU1
  42
  43def electrowealCert : ElectroweakCert where
  44  ew_rank_D := rankEW_eq_D
  45  five_observables := ewObservableCount
  46  rank_sum := ew_from_su2_u1
  47
  48end IndisputableMonolith.Physics.ElectrowealUnificationFromRS

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.