theorem
proved
vev_in_range
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Constants.ElectroweakVEVStructure on GitHub at line 154.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
151noncomputable def vev_canonical : ℝ := 246
152
153/-- The VEV is in the observed range (244, 248) GeV. -/
154theorem vev_in_range : (244 : ℝ) < vev_canonical ∧ vev_canonical < 248 := by
155 unfold vev_canonical; constructor <;> norm_num
156
157/-- The VEV is positive. -/
158theorem vev_canonical_pos : (0 : ℝ) < vev_canonical := by
159 unfold vev_canonical; norm_num
160
161/-- The VEV/electron-mass ratio is on the φ-ladder near rung 27.
162 With v = 246 GeV = 246000 MeV and m_e ≈ 0.511 MeV: ratio ≈ 481408.
163 φ^27 ≈ 514229, within 7%. The φ^27 assignment is the best-fit rung. -/
164theorem vev_electron_rung_27_order :
165 (300000 : ℝ) < (246000 : ℝ) / 0.511 ∧ (246000 : ℝ) / 0.511 < 600000 := by
166 constructor <;> norm_num
167
168end ElectroweakVEVStructure
169end Constants
170end IndisputableMonolith