def
definition
electronMass_GeV
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.ElectroweakBosons on GitHub at line 165.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
162/-! ## φ-Ladder Connection -/
163
164/-- Electron mass in GeV. -/
165def electronMass_GeV : ℝ := 0.000511
166
167/-- W to electron mass ratio. -/
168def w_electron_ratio : ℝ := wBosonMass_GeV / electronMass_GeV
169
170/-- φ^23 is close to the W/e mass ratio scale. -/
171def phi_23 : ℝ := phi ^ 23
172
173/-- φ^24 is close to the Z/e mass ratio scale. -/
174def phi_24 : ℝ := phi ^ 24
175
176/-- VEV in units of electron mass. -/
177def vev_electron_ratio : ℝ := vev_GeV / electronMass_GeV
178
179/-- VEV/m_e ≈ 4.8 × 10^5 ≈ φ^27. -/
180def phi_27 : ℝ := phi ^ 27
181
182/-! ## Higgs Connection -/
183
184/-- Higgs boson mass in GeV. -/
185def higgsMass_GeV : ℝ := 125.25
186
187/-- Higgs to W mass ratio. -/
188def higgs_w_ratio : ℝ := higgsMass_GeV / wBosonMass_GeV
189
190/-- Higgs to W ratio ≈ 1.56 ≈ φ. -/
191theorem higgs_w_near_phi : |higgs_w_ratio - phi| < 0.1 := by
192 -- 125.25 / 80.3692 ≈ 1.5585, φ ∈ (1.61, 1.62)
193 -- |1.5585 - 1.618| ≈ 0.06 < 0.1
194 simp only [higgs_w_ratio, higgsMass_GeV, wBosonMass_GeV]
195 have hphi_lo : phi > 1.61 := phi_gt_onePointSixOne