IndisputableMonolith.Masses.KernelTypes

   1import Mathlib
   2
   3namespace IndisputableMonolith
   4namespace Masses
   5
   6structure GaugeSkeleton where
   7  Y            : ℚ
   8  colorRep     : Bool
   9  isWeakDoublet : Bool
  10
  11structure Completion where
  12  nY : ℤ
  13  n3 : ℤ
  14  n2 : ℤ
  15
  16structure WordLength where
  17  len : GaugeSkeleton → Completion → Nat
  18
  19inductive GenClass | g1 | g2 | g3
  20deriving DecidableEq, Repr
  21
  22@[simp] def tauOf : GenClass → ℤ
  23| .g1 => 0
  24| .g2 => 11
  25| .g3 => 17
  26
  27structure RungSpec where
  28  ell : Nat
  29  gen : GenClass
  30
  31@[simp] def rungOf (R : RungSpec) : ℤ := (R.ell : ℤ) + tauOf R.gen
  32
  33end Masses
  34end IndisputableMonolith
  35