def definition def or abbrev

`sin2ThetaW_RS`

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

formal statement (Lean)

 134noncomputable def sin2ThetaW_RS : ℝ := (3 - phi) / 6

Definition body.

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

row_sin2_thetaW_RS_bracket in IndisputableMonolith.Physics.WeinbergAngleScoreCard decl_use
WeinbergAngleScoreCardCert in IndisputableMonolith.Physics.WeinbergAngleScoreCard decl_use
HiggsRungCert in IndisputableMonolith.StandardModel.HiggsRungAssignment decl_use
mH_prediction_in_interval in IndisputableMonolith.StandardModel.HiggsRungAssignment decl_use
mH_rs_level2 in IndisputableMonolith.StandardModel.HiggsRungAssignment decl_use
mH_rs_level2_in_range in IndisputableMonolith.StandardModel.HiggsRungAssignment decl_use
mH_rs_level3 in IndisputableMonolith.StandardModel.HiggsRungAssignment decl_use
q3_correction_pos in IndisputableMonolith.StandardModel.HiggsRungAssignment decl_use
higgs_rung_prediction in IndisputableMonolith.StandardModel.Q3Representations decl_use
higgs_rung_prediction_pos in IndisputableMonolith.StandardModel.Q3Representations decl_use
sin2ThetaW_RS_approx in IndisputableMonolith.StandardModel.Q3Representations decl_use
sin2ThetaW_RS_lt_half in IndisputableMonolith.StandardModel.Q3Representations decl_use
sin2ThetaW_RS_pos in IndisputableMonolith.StandardModel.Q3Representations decl_use
sin2ThetaW_RS_val in IndisputableMonolith.StandardModel.Q3Representations decl_use