def
definition
phi_23
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 171.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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
196 have hphi_hi : phi < 1.62 := phi_lt_onePointSixTwo
197 have h1 : (125.25 : ℝ) / 80.3692 > 1.55 := by norm_num
198 have h2 : (125.25 : ℝ) / 80.3692 < 1.56 := by norm_num
199 rw [abs_lt]
200 constructor <;> linarith
201