row_mH_pred_interval
plain-language theorem explainer
The level-3 Recognition Science Higgs mass lies strictly between 120 and 130 GeV. Collider physicists comparing RS mass ladders to LHC data cite this interval when scoring the Higgs prediction against the observed 125.2 GeV value. The proof is a one-line wrapper that directly invokes the upstream interval theorem from the Higgs rung assignment module.
Claim. The level-3 Recognition Science Higgs mass satisfies $120 < m_H^{RS,3} < 130$, where $m_H^{RS,3} = v_0 sqrt(sin^2 theta_W^{RS} * 17/16)$ with $v_0 = 246$ GeV and $sin^2 theta_W^{RS} = (3 - phi)/6$.
background
In the Higgs mass scorecard module the level-3 prediction is defined as $mH_rs_level3 = vev * sqrt(sin2ThetaW_RS * 17/16)$. Here vev is the electroweak symmetry breaking scale fixed at 246 GeV for display, sin2ThetaW_RS equals (3 - phi)/6 with phi the golden-ratio fixed point, and the factor 17/16 encodes the Q3 mode budget (16 addressing modes plus the physical Higgs singlet). The upstream theorem mH_prediction_in_interval establishes the same numerical bound by applying nlinarith to the product bounds phi_lt_onePointSixTwo and phi_gt_onePointSixOne.
proof idea
The proof is a one-line wrapper that applies the upstream theorem mH_prediction_in_interval.
why it matters
This interval is referenced by higgsMassScoreCardCert_holds to build the certificate that records both the (120,130) window and the five-percent proximity to the observed mass. It completes the P2-HIGGS scorecard step in the Recognition Science chain, where the phi-ladder mass formula yields a prediction inside the experimental band. The full one-loop electroweak correction remains an open formalization task.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.