mH_rs_level2_in_range
plain-language theorem explainer
The RS level-2 Higgs mass prediction lies strictly between 110 and 125 GeV. Particle physicists comparing the phi-ladder mass table to LHC data would cite this bound when checking the basic sin^2 theta_W scaling. The proof unfolds the definition to 246 times the square root of (3-phi)/6, uses the supplied phi bounds to pin that quantity between 0.228 and 0.233, and verifies the target inequalities by comparing squares and applying sqrt monotonicity.
Claim. $110 < 246 sqrt((3 - phi)/6) < 125$, where the expression is the level-2 RS Higgs mass obtained from the vacuum expectation value and the Weinberg angle sin^2 theta_W = (3 - phi)/6.
background
In the Recognition Science treatment of the Standard Model the Higgs mass is read off the phi-ladder after symmetry breaking. The level-2 formula is m_H = v sqrt(sin^2 theta_W) with v fixed at 246 GeV and sin^2 theta_W = (3 - phi)/6; the latter follows from the forced Weinberg angle proved in the companion module. Upstream lemmas supply the tight numerical bounds phi > 1.61 and phi < 1.62 that translate directly into 0.228 < sin^2 theta_W < 0.233.
proof idea
The tactic proof unfolds mH_rs_level2, vev and sin2ThetaW_RS. It obtains the interval for (3-phi)/6 by linarith applied to the two phi bounds, then proves the lower target by showing (110/246)^2 lies below the lower bound on sin^2 and invoking sqrt_lt_sqrt followed by multiplication by 246. The upper target is obtained symmetrically by comparing (125/246)^2 to the upper bound on sin^2 and repeating the square-root step.
why it matters
The theorem supplies the level2_range component of higgsRungCert, the certificate that assembles all RS Higgs bounds. It completes the level-2 rung assignment inside the Higgs mass derivation, confirming that the basic scaling already lands inside the observed window before the Q3 1/16 correction is added. The result sits inside the T5-T8 forcing chain that produces the phi-ladder and the eight-tick octave used for mass quantization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.