theorem
proved
rankEW_eq_D
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.ElectrowealUnificationFromRS on GitHub at line 29.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
26def rankU1 : ℕ := 1
27def rankEW : ℕ := rankSU2 + rankU1
28
29theorem rankEW_eq_D : rankEW = 3 := by decide
30theorem ew_from_su2_u1 : rankEW = rankSU2 + rankU1 := rfl
31
32inductive EWObservable where
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