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)
182theorem conjugate_dim_forced :
183 V 3 - (SpectralSector.dim .color +
184 SpectralSector.dim .weak +
185 SpectralSector.dim .hypercharge) =
186 SpectralSector.dim .conjugate := by
proof body
Term-mode proof.
187 norm_num [V, SpectralSector.dim]
188
189/-- **THEOREM**: Total gauge generators: 8 + 3 + 1 = 12 = |E(Q₃)|.
190 The gauge degrees of freedom equal the edge count of Q₃. -/
depends on (12)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
V
in IndisputableMonolith.Cosmology.InflatonPotentialFromJCost
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
E
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
SpectralSector
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
V
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
dim
in IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation
decl_use
-
SpectralSector
in IndisputableMonolith.Physics.RecognitionHamiltonianSpectrum
decl_use
-
V
in IndisputableMonolith.RRF.Core.Glossary
decl_use