def
definition
phi_27
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 180.
browse module
All declarations in this module, on Recognition.
explainer page
formal source
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
202/-- Z to W ratio ≈ 1.135. -/
203def z_w_ratio : ℝ := zBosonMass_GeV / wBosonMass_GeV
204
205theorem z_w_ratio_approx : |z_w_ratio - 1.135| < 0.01 := by
206 -- 91.1876 / 80.3692 = 1.1346..., |1.1346 - 1.135| = 0.0004 < 0.01
207 simp only [z_w_ratio, zBosonMass_GeV, wBosonMass_GeV]
208 norm_num
209
210/-! ## Electroweak Unification Scale -/