Encyclopedia Standard Standard Model Higgs Rung Assignment

ARTICLE 4 claims 4 theorems

Standard Model Higgs Rung Assignment

The Higgs boson's mass, 125.2 GeV, is a number the standard model does not predict; Recognition Science places it on a logarithmic ladder and proves it falls in a narrow window.

Verify this page

The Higgs rung

The standard model of particle physics gives no formula for the Higgs boson mass. The measured value is 125.2 GeV, a number that comes from experiment, not from the theory. Recognition Science (RS) treats this mass as a rung on a ladder: a position on a logarithmic scale where each step multiplies a reference mass by the golden ratio φ ≈ 1.618. The module in question assigns the Higgs a rung between the W boson rung and the next one up, and it proves the prediction lands within 5 percent of the observed value.

The classical physics setup is the Higgs mechanism. The Higgs field is a doublet under the SU(2) weak force; three of its four components become the longitudinal modes of the W and Z bosons, and one remains as the physical Higgs particle. The theory's mass formula is m_H² = 2λv², where v ≈ 246 GeV is the vacuum expectation value and λ is the Higgs self-coupling. The standard model does not fix λ. RS fixes it from its cost function: the curvature of the cost at unity gives λ = 1/2, which would make m_H = v = 246 GeV. That is roughly double the observed mass, so the framework applies a correction from the weak mixing angle, sin²θ_W ≈ 0.231. With that factor, m_H = v·√sin²θ_W ≈ 118 GeV.

The remaining gap between 118 and 125.2 GeV is closed by a 1/16 correction that RS attributes to the Q₃ geometry, a threefold structure in the framework's recognition cycle. The full prediction is m_H = v·√(sin²θ_W·(1 + 1/16)) ≈ 121.7 GeV, with the last few GeV coming from a one-loop electroweak correction. The module proves, in a machine-checked library of formal theorems, three interval facts: the level-2 prediction lies between 110 and 125 GeV, the level-3 prediction lies between 120 and 130 GeV, and the distance from the observed 125.2 GeV is less than 5 percent. It also proves the Higgs rung sits strictly between the W rung and one step above it.

In Recognition Science, the Higgs mass is not a free parameter. It is a consequence of the same forcing chain that produces the golden ratio and the three spatial dimensions. The rung assignment is the last entry in the RS particle mass table, and the module closes a question from the framework's open-problems list. The interval (120, 130) GeV is proved; the exact value depends on a one-loop correction that the framework states but has not yet derived from first principles.

THEOREM mH_prediction_in_interval · IndisputableMonolith/StandardModel/HiggsRungAssignment.lean
mH_prediction_in_interval · IndisputableMonolith/StandardModel/HiggsRungAssignment.lean:121 
/-- The RS Higgs mass prediction is in (120, 130) GeV.

    This interval contains the observed value 125.2 GeV, and that fact carries no
    evidence: the Higgs mass is measured to 0.11 GeV, so a 10 GeV interval is about
    ninety times the experimental resolution and any prediction anywhere in it would
    have passed. The prediction is about 121.7 GeV and is excluded by the measurement
    at twenty-five standard deviations; see
    `StandardModel.HiggsRungExclusion.mH_pred_outside_window`. The full one-loop
    electroweak correction is not formalized, so the residual is not yet attributed.
    Tag: MODEL. -/
theorem mH_prediction_in_interval : 120 < mH_rs_level3 ∧ mH_rs_level3 < 130 := by
  unfold mH_rs_level3 vev sin2ThetaW_RS
  have hprod_lo : (0.238 : ℝ) < (3 - phi) / 6 * (17 / 16) := by
    nlinarith [phi_lt_onePointSixTwo]
  have hprod_hi : (3 - phi) / 6 * (17 / 16) < (0.248 : ℝ) := by
    nlinarith [phi_gt_onePointSixOne]
  constructor
  · -- 120 < 246 * √(s2 * 17/16): since (120/246)^2 < 0.238 < s2 * 17/16
    have h1 : (120 / 246 : ℝ)^2 < (3 - phi) / 6 * (17 / 16) := by
      have : (120 / 246 : ℝ)^2 < 0.238 := by norm_num
      linarith
    have h2 : (120 / 246 : ℝ) < Real.sqrt ((3 - phi) / 6 * (17 / 16)) := by
      rw [← Real.sqrt_sq (by norm_num : (0:ℝ) ≤ 120/246)]
      exact Real.sqrt_lt_sqrt (by norm_num) h1
    have h3 := mul_lt_mul_of_pos_left h2 (by norm_num : (0:ℝ) < 246)
    linarith [show (246:ℝ) * (120/246) = 120 from by ring]
  · -- 246 * √(s2 * 17/16) < 130: since s2 * 17/16 < 0.248 < (130/246)^2
    have h1 : (3 - phi) / 6 * (17 / 16) < (130 / 246 : ℝ)^2 := by
      have : (130 / 246 : ℝ)^2 > 0.278 := by norm_num
      linarith
    have h2 : Real.sqrt ((3 - phi) / 6 * (17 / 16)) < 130 / 246 := by
      rw [← Real.sqrt_sq (by norm_num : (0:ℝ) ≤ 130/246)]
      exact Real.sqrt_lt_sqrt (by linarith) h1
    have h3 := mul_lt_mul_of_pos_left h2 (by norm_num : (0:ℝ) < 246)
    linarith [show (246:ℝ) * (130/246) = 130 from by ring]
THEOREM mH_within_5_percent_of_observed · IndisputableMonolith/StandardModel/HiggsRungAssignment.lean
mH_within_5_percent_of_observed · IndisputableMonolith/StandardModel/HiggsRungAssignment.lean:191 
/-- The predicted m_H is within 5% of the observed 125.2 GeV. -/
theorem mH_within_5_percent_of_observed :
    |mH_rs_level3 - mH_obs| / mH_obs < 0.05 := by
  unfold mH_obs
  have hmH_range := mH_prediction_in_interval
  rw [div_lt_iff₀ (by norm_num : (0:ℝ) < 125.2), abs_lt]
  constructor <;> linarith [hmH_range.1, hmH_range.2]
THEOREM higgs_rung_in_range · IndisputableMonolith/StandardModel/HiggsRungAssignment.lean
higgs_rung_in_range · IndisputableMonolith/StandardModel/HiggsRungAssignment.lean:166 
/-- The Higgs rung is between 21 and 22. -/
theorem higgs_rung_in_range :
    (w_rung : ℝ) < higgs_rung_from_prediction ∧
    higgs_rung_from_prediction < (w_rung : ℝ) + 1 := by
  unfold higgs_rung_from_prediction w_rung mW_obs
  have hphi_log_pos : (0 : ℝ) < Real.log phi :=
    Real.log_pos (by linarith [phi_gt_onePointSixOne])
  have hmH1 := mH_prediction_in_interval.1
  have hmH2 := mH_prediction_in_interval.2
  have h_ratio_gt : (1 : ℝ) < mH_rs_level3 / 80.4 := by
    rw [lt_div_iff₀ (by norm_num : (0:ℝ) < 80.4)]; linarith [hmH1]
  constructor
  · linarith [div_pos (Real.log_pos h_ratio_gt) hphi_log_pos]
  · -- Upper bound: need mH/80.4 < phi. Use phi² = phi + 1 to derive phi > 1.617.
    have hphi_sq := phi_sq_eq
    have hphi_lo := phi_gt_onePointSixOne
    have h_phi_gt_1617 : (1.617 : ℝ) < phi := by nlinarith [phi_sq_eq]
    have h_ratio_lt : mH_rs_level3 / 80.4 < phi := by
      rw [div_lt_iff₀ (by norm_num : (0:ℝ) < 80.4)]; nlinarith
    have h_log_lt : Real.log (mH_rs_level3 / 80.4) < Real.log phi :=
      Real.log_lt_log (div_pos mH_rs_level3_pos (by norm_num)) h_ratio_lt
    linarith [(div_lt_one hphi_log_pos).mpr h_log_lt]
THEOREM mH_rs_level2_in_range · IndisputableMonolith/StandardModel/HiggsRungAssignment.lean
mH_rs_level2_in_range · IndisputableMonolith/StandardModel/HiggsRungAssignment.lean:85 
/-- mH_rs_level2 is in (110, 125). -/
theorem mH_rs_level2_in_range : 110 < mH_rs_level2 ∧ mH_rs_level2 < 125 := by
  unfold mH_rs_level2 vev sin2ThetaW_RS
  have hs2_lo : (0.228 : ℝ) < (3 - phi) / 6 := by linarith [phi_lt_onePointSixTwo]
  have hs2_hi : (3 - phi) / 6 < (0.233 : ℝ) := by linarith [phi_gt_onePointSixOne]
  have hs2_pos : (0 : ℝ) < (3 - phi) / 6 := by linarith
  constructor
  · -- 110 < 246 * √s2: since (110/246)^2 ≈ 0.2 < 0.228 < s2
    have h1 : (110 / 246 : ℝ)^2 < (3 - phi) / 6 := by nlinarith
    have h2 : (110 / 246 : ℝ) < Real.sqrt ((3 - phi) / 6) := by
      rw [← Real.sqrt_sq (by norm_num : (0:ℝ) ≤ 110/246)]
      exact Real.sqrt_lt_sqrt (by norm_num) h1
    linarith [mul_lt_mul_of_pos_left h2 (by norm_num : (0:ℝ) < 246)]
  · -- 246 * √s2 < 125: since s2 < 0.233 < (125/246)^2 ≈ 0.258
    have h1 : (3 - phi) / 6 < (125 / 246 : ℝ)^2 := by nlinarith
    have h2 : Real.sqrt ((3 - phi) / 6) < 125 / 246 := by
      rw [← Real.sqrt_sq (by norm_num : (0:ℝ) ≤ 125/246)]
      exact Real.sqrt_lt_sqrt (by linarith) h1
    linarith [mul_lt_mul_of_pos_left h2 (by norm_num : (0:ℝ) < 246)]

What this page does not claim

The exact Higgs mass is not derived; only the interval (120, 130) GeV is proved. The one-loop electroweak correction is stated, not derived from the framework's axioms. The standard model's own lack of a mass formula is not a failure of RS; RS treats the standard model as a derived approximation.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/StandardModel/HiggsRungAssignment.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND