`vev`

definition

show as: view math explainer →

module: IndisputableMonolith.StandardModel.HiggsRungAssignment
domain: StandardModel
line: 60 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.StandardModel.HiggsRungAssignment on GitHub at line 60.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  57/-! ## Physical Input Values -/
  58
  59/-- Higgs VEV v ≈ 246 GeV (electroweak scale). -/
  60noncomputable def vev : ℝ := 246
  61
  62/-- W-boson observed mass in GeV. -/
  63noncomputable def mW_obs : ℝ := 80.4
  64
  65/-- Z-boson observed mass in GeV. -/
  66noncomputable def mZ_obs : ℝ := 91.2
  67
  68/-- Higgs observed mass in GeV. -/
  69noncomputable def mH_obs : ℝ := 125.2
  70
  71/-- The VEV is positive. -/
  72theorem vev_pos : 0 < vev := by unfold vev; norm_num
  73
  74/-! ## RS Higgs Mass Prediction -/
  75
  76/-- Level 1: "Naive" RS prediction from m_H = v.
  77    This follows from λ_RS = 1/2, m_H² = 2λv² = v². -/
  78noncomputable def mH_naive : ℝ := vev
  79
  80/-- Level 2: RS prediction with sin²θ_W correction.
  81    m_H = v · √(sin²θ_W) — the dominant correction from Q₃ symmetry breaking. -/
  82noncomputable def mH_rs_level2 : ℝ :=
  83  vev * Real.sqrt sin2ThetaW_RS
  84
  85/-- mH_rs_level2 is in (110, 125). -/
  86theorem mH_rs_level2_in_range : 110 < mH_rs_level2 ∧ mH_rs_level2 < 125 := by
  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.