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)
26inductive SMLagrangianSector where
27 | gaugeKinetic | fermionKinetic | yukawa | higgsPotential | thetaTerm
28 deriving DecidableEq, Repr, BEq, Fintype
29
used by (7)
From the project-wide theorem graph. These declarations reference this one in their body.
-
sector_count
in IndisputableMonolith.Foundation.QRFT.SMLagrangianSkeleton
decl_use
-
SMLagrangianCert
in IndisputableMonolith.Foundation.QRFT.SMLagrangianSkeleton
decl_use
-
SMLagrangianSector
in IndisputableMonolith.Foundation.QRFT.SMLagrangianSkeleton
decl_use
-
totalCost
in IndisputableMonolith.Foundation.QRFT.SMLagrangianSkeleton
decl_use
-
totalCost_nonneg
in IndisputableMonolith.Foundation.QRFT.SMLagrangianSkeleton
decl_use
-
SMLagrangianCert
in IndisputableMonolith.Physics.StandardModelLagrangianStructure
decl_use
-
smSectorCount
in IndisputableMonolith.Physics.StandardModelLagrangianStructure
decl_use
depends on (3)
Lean names referenced from this declaration's body.
-
higgsPotential
in IndisputableMonolith.Foundation.QRFT.HiggsPotentialFromRecognitionVacuum
decl_use
-
SMLagrangianSector
in IndisputableMonolith.Foundation.QRFT.SMLagrangianSkeleton
decl_use
-
higgsPotential
in IndisputableMonolith.StandardModel.ElectroweakBreaking
decl_use