module module

`IndisputableMonolith.StandardModel.Q3Representations`

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 (2)

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

IndisputableMonolith.Physics.WeinbergAngleScoreCard module_import
IndisputableMonolith.StandardModel.HiggsRungAssignment module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (24)

inductive Q3Element L56
def Spin0Sector L68
def Spin1Sector L71
theorem spin0_count L77
theorem spin1_count L80
theorem q3_order L83
def casimir L88
theorem spin0_casimir L91
theorem spin1_casimir L94
theorem casimir_ratio_undefined L98
def lambda_RS L104
theorem lambda_RS_val L106
def higgsMassSq_over_vev L110
theorem higgsMassSq_simplifies L112
def wMassSq_over_vev L118
def higgsMassRatio L121
def sin2ThetaW_RS L134
theorem sin2ThetaW_RS_val L136
theorem sin2ThetaW_RS_pos L139
theorem sin2ThetaW_RS_lt_half L146
theorem sin2ThetaW_RS_approx L152
def w_rung L163
def higgs_rung_prediction L184
theorem higgs_rung_prediction_pos L191