def definition def or abbrev

`mH_rs_level3`

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

formal statement (Lean)

 109noncomputable def mH_rs_level3 : ℝ :=

Definition body.

 110  vev * Real.sqrt (sin2ThetaW_RS * (17 / 16))
 111
 112/-- The Q₃ correction factor 17/16 is positive. -/

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

HiggsMassScoreCardCert in IndisputableMonolith.Physics.HiggsMassScoreCard decl_use
row_mH_pred_interval in IndisputableMonolith.Physics.HiggsMassScoreCard decl_use
row_mH_within_five_percent in IndisputableMonolith.Physics.HiggsMassScoreCard decl_use
HiggsRungCert in IndisputableMonolith.StandardModel.HiggsRungAssignment decl_use
higgs_rung_from_prediction in IndisputableMonolith.StandardModel.HiggsRungAssignment decl_use
higgs_rung_in_range in IndisputableMonolith.StandardModel.HiggsRungAssignment decl_use
mH_prediction_in_interval in IndisputableMonolith.StandardModel.HiggsRungAssignment decl_use
mH_rs_level3_pos in IndisputableMonolith.StandardModel.HiggsRungAssignment decl_use
mH_within_5_percent_of_observed in IndisputableMonolith.StandardModel.HiggsRungAssignment decl_use
q3_correction_pos in IndisputableMonolith.StandardModel.HiggsRungAssignment decl_use

Lean names referenced from this declaration's body.

is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
correction in IndisputableMonolith.Information.QuantumChannelCapacityFromPhi decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
vev in IndisputableMonolith.QFT.HiggsMechanism decl_use
vev in IndisputableMonolith.StandardModel.ElectroweakBreaking decl_use
vev in IndisputableMonolith.StandardModel.HiggsRungAssignment decl_use
sin2ThetaW_RS in IndisputableMonolith.StandardModel.Q3Representations decl_use