No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
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 -/
162
163/-- **THEOREM**: Sector dimensions sum to 8 = |V(Q₃)|.
164 The spectral decomposition accounts for every vertex. -/
used by (10)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (32)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
Dimension
in IndisputableMonolith.Constants.Dimensions
decl_use
-
Dimension
in IndisputableMonolith.Constants.Dimensions
decl_use
-
U
in IndisputableMonolith.Constants.RSNativeUnits
decl_use
-
V
in IndisputableMonolith.Cosmology.InflatonPotentialFromJCost
decl_use
-
has
in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
Dimension
in IndisputableMonolith.Foundation.DimensionForcing
decl_use
-
Dimension
in IndisputableMonolith.Foundation.DimensionForcing
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
rank
in IndisputableMonolith.Foundation.PreTemporalForcingOrder
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
V
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
for
in IndisputableMonolith.Foundation.UniversalForcingSelfReference
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
Sector
in IndisputableMonolith.Masses.Anchor
decl_use
-
Sector
in IndisputableMonolith.Masses.RSBridge.Anchor
decl_use
-
Sector
in IndisputableMonolith.Masses.RungConstructor.Basic
decl_use
-
dim
in IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation
decl_use
-
SpectralSector
in IndisputableMonolith.Physics.RecognitionHamiltonianSpectrum
decl_use
-
SpectralSector
in IndisputableMonolith.Physics.RecognitionHamiltonianSpectrum
decl_use
-
SpectralSector
in IndisputableMonolith.Physics.RecognitionHamiltonianSpectrum
decl_use
-
SpectralSector
in IndisputableMonolith.Physics.RecognitionHamiltonianSpectrum
decl_use
-
U
in IndisputableMonolith.Recognition
decl_use
-
V
in IndisputableMonolith.RRF.Core.Glossary
decl_use
… and 2 more