row_mH_pred_interval
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the vev or Weinberg angle from the J-cost functional equation.
- Does not incorporate higher-order electroweak corrections beyond the Q3 factor.
- Does not claim the prediction is exact, only that it lies inside the stated interval under the given inputs.
Lean usage
have h : 120 < mH_rs_level3 ∧ mH_rs_level3 < 130 := row_mH_pred_intervalformal statement (Lean)
36theorem row_mH_pred_interval :
37 120 < mH_rs_level3 ∧ mH_rs_level3 < 130 := mH_prediction_in_interval
proof body
38