`uGenCount`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.SMGaugeAlgebra
domain: Foundation
line: 30 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.SMGaugeAlgebra on GitHub at line 30.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

used by

factorGenCount IndisputableMonolith.Foundation.SMGaugeAlgebra

formal source

  27def suGenCount (N : ℕ) : ℕ := N * N - 1
  28
  29/-- Number of generators of `u(N)` is `N²`. -/
  30def uGenCount (N : ℕ) : ℕ := N * N
  31
  32/-- The three SM gauge factors. -/
  33inductive SMGaugeFactor where
  34  | strong  -- SU(3): 8 generators
  35  | weak    -- SU(2): 3 generators
  36  | hyperY  -- U(1): 1 generator
  37  deriving DecidableEq, Repr, BEq, Fintype
  38
  39/-- Generator count per gauge factor. -/
  40def factorGenCount : SMGaugeFactor → ℕ
  41  | .strong => suGenCount 3
  42  | .weak   => suGenCount 2
  43  | .hyperY => uGenCount 1
  44
  45theorem strong_gen_count : factorGenCount .strong = 8 := by decide
  46theorem weak_gen_count : factorGenCount .weak = 3 := by decide
  47theorem hyper_gen_count : factorGenCount .hyperY = 1 := by decide
  48
  49/-- Total SM gauge-generator count. -/
  50def smTotalGenCount : ℕ :=
  51  factorGenCount .strong + factorGenCount .weak + factorGenCount .hyperY
  52
  53theorem sm_total_gen_count : smTotalGenCount = 12 := by decide
  54
  55/-- Number of SM gauge factors = 3, matching the cube-automorphism
  56three-layer decomposition. -/
  57theorem factor_count : Fintype.card SMGaugeFactor = 3 := by decide
  58
  59structure SMGaugeAlgebraCert where
  60  strong : factorGenCount .strong = 8

papers checked against this theorem

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