module module

`IndisputableMonolith.Foundation.SMHyperchargeFromCube`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Foundation.UnifiedForcingChain module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.GaugeLieCompletionFromCube module_import

declarations in this module (25)

inductive WeylMultiplet L48
theorem weylMultiplet_count L57
def weylMultiplicity L61
def hypercharge6 L70
def higgsHypercharge6 L79
theorem higgsHypercharge6_eq L81
def generationWeylStateCount L84
theorem generationWeylStateCount_eq_16 L92
def threeGenerationWeylStateCount L96
theorem threeGenerationWeylStateCount_eq_48 L98
def su3SquaredU1Anomaly6 L106
theorem su3SquaredU1Anomaly6_eq_zero L111
def su2SquaredU1Anomaly6 L115
theorem su2SquaredU1Anomaly6_eq_zero L119
def gravitationalU1Anomaly6 L123
theorem gravitationalU1Anomaly6_eq_zero L131
def cubicU1Anomaly6 L135
theorem cubicU1Anomaly6_eq_zero L143
inductive WeakComponent L149
def weakT3_6 L154
def electricCharge6 L159
theorem quark_doublet_charges L162
theorem lepton_doublet_charges L167
structure SMHyperchargeCert L172
def smHyperchargeCert L187