mH_within_5_percent_of_observed
plain-language theorem explainer
The RS level-3 Higgs mass prediction satisfies |mH_rs_level3 - 125.2| / 125.2 < 0.05. Model builders comparing the phi-ladder output to collider data would reference this bound. The proof unfolds the observed mass definition, invokes the established (120,130) interval theorem, and reduces the percentage deviation via division and absolute value lemmas followed by linear arithmetic.
Claim. $|m_H^{RS,3} - 125.2| / 125.2 < 0.05$, where $m_H^{RS,3} = v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v_e v
background
The module derives the Higgs boson mass from the phi-ladder using Q3 geometry to complete the RS particle mass table. mH_rs_level3 is defined as vev times the square root of sin2ThetaW_RS times 17/16, where the 17/16 factor encodes the Q3 mode budget (one extra singlet mode out of 16 total). sin2ThetaW_RS equals (3 - phi)/6 from the Weinberg angle module. The upstream theorem mH_prediction_in_interval establishes that this expression lies strictly between 120 and 130 GeV, containing the observed value.
proof idea
Term-mode proof. It unfolds mH_obs to the constant 125.2, obtains the closed interval bounds from mH_prediction_in_interval, rewrites the target percentage inequality via div_lt_iff0 and abs_lt, then splits into two one-sided inequalities solved directly by linarith on the interval endpoints.
why it matters
This theorem supplies the within-5-percent clause for both higgsRungCert and higgsMassScoreCardCert_holds, confirming the level-3 rung assignment for the Higgs. It closes the module hypothesis that the phi-ladder plus Q3 correction places mH inside (120,130) GeV, linking the J-cost curvature and Weinberg angle to the observed spectrum without requiring further scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.