mH_prediction_in_interval
plain-language theorem explainer
The RS level-three Higgs mass prediction lies strictly between 120 and 130 GeV. Researchers building the phi-ladder particle spectrum cite this bound to confirm consistency with the observed 125.2 GeV value. The proof unfolds the mass expression, bounds the product involving (3-phi)/6 times 17/16 via nlinarith on the golden-ratio inequalities, then verifies the square-root comparisons to 120/246 and 130/246 with norm_num and linarith.
Claim. The Recognition Science level-three Higgs mass satisfies $120 < m_H < 130$ in GeV units, where $m_H = 246 · √[((3-φ)/6) · (17/16)]$ and $φ$ is the golden ratio.
background
The module derives the Higgs mass from the phi-ladder using Q3 geometry after the electroweak symmetry breaking. The vacuum expectation value is fixed near 246 GeV. The Weinberg angle factor is sin²θ_W = (3-φ)/6, proved upstream in the WeinbergAngle module. The level-three formula adds the 1/16 Q3 correction, so m_H = vev · √(sin²θ_W · 17/16). Upstream lemmas supply the tight bounds 1.61 < φ < 1.62 that pin the numerical interval.
proof idea
The tactic proof unfolds mH_rs_level3 and sin2ThetaW_RS. It first proves the product (3-φ)/6 · 17/16 lies between 0.238 and 0.248 using nlinarith with phi_lt_onePointSixTwo and phi_gt_onePointSixOne. For the lower bound it shows (120/246)² < product, takes square roots, and multiplies by 246. The upper bound follows by the symmetric comparison to (130/246)², again using sqrt_lt_sqrt and mul_lt_mul_of_pos_left.
why it matters
This theorem is invoked directly by higgsRungCert to certify the full Higgs rung assignment and by mH_within_5_percent_of_observed to establish agreement within 5 percent of the measured mass. It completes the RS particle mass table in the StandardModel module and closes the (120,130) GeV hypothesis interval. The derivation rests on the J-cost curvature and the phi self-similar fixed point from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.