IndisputableMonolith.Foundation.SMGaugeAlgebra

   1import Mathlib
   2
   3/-!
   4# SM Gauge Algebra: Generator Counts of SU(3) × SU(2) × U(1)
   5
   6The cube-automorphism cert (`IndisputableMonolith/Foundation/GaugeFromCube`)
   7proves the rank decomposition `B₃ = (ℤ/2)³ ⋊ S₃` matches the SM gauge
   8group ranks (3, 2, 1). The structural-rank cert
   9(`Foundation/GaugeGroupStructure`) is honestly tagged STARTED. This
  10module adds the Lie-algebra-level structure: the canonical generator
  11counts `(8, 3, 1)` for `(su(3), su(2), u(1))` matching the dimensions
  12`(N²-1, N²-1, 1)` for `(N=3, N=2, N=1)`.
  13
  14The 8 + 3 + 1 = 12 total gauge generators match the empirical SM count.
  15The structural prediction: any RS-derived gauge group with the same
  16cube-automorphism rank decomposition has exactly 12 generators; any
  17deviation would falsify the gauge-group-from-cube identification.
  18
  19Lean status: 0 sorry, 0 axiom.
  20-/
  21
  22namespace IndisputableMonolith
  23namespace Foundation
  24namespace SMGaugeAlgebra
  25
  26/-- Number of generators of `su(N)` is `N² - 1`. -/
  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
  61  weak : factorGenCount .weak = 3
  62  hyperY : factorGenCount .hyperY = 1
  63  total : smTotalGenCount = 12
  64  factor_count : Fintype.card SMGaugeFactor = 3
  65
  66/-- SM gauge-algebra certificate. -/
  67def smGaugeAlgebraCert : SMGaugeAlgebraCert where
  68  strong := strong_gen_count
  69  weak := weak_gen_count
  70  hyperY := hyper_gen_count
  71  total := sm_total_gen_count
  72  factor_count := factor_count
  73
  74end SMGaugeAlgebra
  75end Foundation
  76end IndisputableMonolith
  77