inductive
definition
SpectralSector
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.SpectralEmergence on GitHub at line 131.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
of -
of -
Dimension -
Dimension -
U -
V -
has -
of -
of -
Dimension -
Dimension -
of -
of -
rank -
of -
of -
V -
for -
of -
of -
Sector -
Sector -
Sector -
dim -
SpectralSector -
SpectralSector -
SpectralSector -
SpectralSector -
U -
V -
rank -
Sector
used by
formal source
128 - **Conjugate**: the residual 2-dimensional sector, dim 2
129
130 The total: 3 + 2 + 1 + 2 = 8 = |V(Q₃)| = 2^D. -/
131inductive SpectralSector where
132 | color : SpectralSector
133 | weak : SpectralSector
134 | hypercharge : SpectralSector
135 | conjugate : SpectralSector
136 deriving DecidableEq, Repr
137
138/-- Dimension of each spectral sector. -/
139def SpectralSector.dim : SpectralSector → ℕ
140 | .color => 3
141 | .weak => 2
142 | .hypercharge => 1
143 | .conjugate => 2
144
145/-- The gauge group rank (dimension of the Lie algebra generators)
146 associated with each sector. -/
147def SpectralSector.gauge_rank : SpectralSector → ℕ
148 | .color => 8 -- SU(3): 3²-1 = 8 generators
149 | .weak => 3 -- SU(2): 2²-1 = 3 generators
150 | .hypercharge => 1 -- U(1): 1 generator
151 | .conjugate => 0 -- Not a gauge sector
152
153/-- The matter representation dimension (how many components
154 a fermion field has in this sector). -/
155def SpectralSector.matter_dim : SpectralSector → ℕ
156 | .color => 3
157 | .weak => 2
158 | .hypercharge => 1
159 | .conjugate => 2
160
161/-! ### Sector Dimension Theorems -/