mH_rs_level2_in_range
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 in Recognition Science
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.
scope and limits
- Does not compute the exact numerical value of the Higgs mass.
- Does not incorporate the Q3 1/16 mode-budget correction.
- Does not address one-loop electroweak corrections beyond the basic scaling.
- Does not establish the level-3 prediction interval.
formal statement (Lean)
86theorem mH_rs_level2_in_range : 110 < mH_rs_level2 ∧ mH_rs_level2 < 125 := by
proof body
Tactic-mode proof.
87 unfold mH_rs_level2 vev sin2ThetaW_RS
88 have hs2_lo : (0.228 : ℝ) < (3 - phi) / 6 := by linarith [phi_lt_onePointSixTwo]
89 have hs2_hi : (3 - phi) / 6 < (0.233 : ℝ) := by linarith [phi_gt_onePointSixOne]
90 have hs2_pos : (0 : ℝ) < (3 - phi) / 6 := by linarith
91 constructor
92 · -- 110 < 246 * √s2: since (110/246)^2 ≈ 0.2 < 0.228 < s2
93 have h1 : (110 / 246 : ℝ)^2 < (3 - phi) / 6 := by nlinarith
94 have h2 : (110 / 246 : ℝ) < Real.sqrt ((3 - phi) / 6) := by
95 rw [← Real.sqrt_sq (by norm_num : (0:ℝ) ≤ 110/246)]
96 exact Real.sqrt_lt_sqrt (by norm_num) h1
97 linarith [mul_lt_mul_of_pos_left h2 (by norm_num : (0:ℝ) < 246)]
98 · -- 246 * √s2 < 125: since s2 < 0.233 < (125/246)^2 ≈ 0.258
99 have h1 : (3 - phi) / 6 < (125 / 246 : ℝ)^2 := by nlinarith
100 have h2 : Real.sqrt ((3 - phi) / 6) < 125 / 246 := by
101 rw [← Real.sqrt_sq (by norm_num : (0:ℝ) ≤ 125/246)]
102 exact Real.sqrt_lt_sqrt (by linarith) h1
103 linarith [mul_lt_mul_of_pos_left h2 (by norm_num : (0:ℝ) < 246)]
104
105/-- Level 3: RS prediction with Q₃ 1/16 correction factor.
106 m_H = v · √(sin²θ_W · 17/16)
107 The factor 17/16 = 1 + 1/16 comes from the Q₃ mode budget:
108 16 addressing modes total, 17th = the physical Higgs singlet mode. -/