pith. sign in
def

mH_rs_level3

definition
show as:
module
IndisputableMonolith.StandardModel.HiggsRungAssignment
domain
StandardModel
line
109 · github
papers citing
none yet

plain-language theorem explainer

The mH_rs_level3 definition supplies the Recognition Science level-3 Higgs mass as the vacuum expectation value scaled by the square root of the Weinberg angle times the Q3 correction factor 17/16. Particle physicists scoring the Standard Model Higgs prediction against LHC data cite this expression to verify the (120, 130) GeV interval and 5% agreement with the observed mass. It is realized as a direct term-mode combination of the vev and sin2ThetaW_RS constants.

Claim. $m_H = v · √(sin²θ_W · 17/16)$ where $v$ is the vacuum expectation value and $sin²θ_W$ is the RS Weinberg angle.

background

The HiggsRungAssignment module derives the Higgs boson mass from the φ-ladder using Q3 geometry. The vacuum expectation value is defined as phi in the upstream QFT.HiggsMechanism.vev declaration. The Weinberg angle sin2ThetaW_RS equals (3-φ)/6 as established in the sibling WeinbergAngle module. The factor 17/16 encodes the Q3 mode budget: 16 addressing modes plus the physical Higgs singlet mode, per the module doc-comment.

proof idea

The definition is a one-line term-mode expression that directly assembles the level-3 prediction from the already-established vev and sin2ThetaW_RS constants.

why it matters

This definition supplies the numerical value asserted by the downstream HiggsMassScoreCardCert structure, which requires both 120 < mH_rs_level3 < 130 and |mH_rs_level3 - mH_obs| / mH_obs < 0.05. It completes the level-3 rung assignment in the module and supports the hypothesis that the RS framework reproduces the Higgs mass. It touches the open question of the exact one-loop EW correction for precise matching to 125.2 GeV.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.