def
definition
weinbergAngle
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.StandardModel.WZMassRatio on GitHub at line 61.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
58 constructor <;> norm_num
59
60/-- The Weinberg angle θ_W (weak mixing angle). -/
61noncomputable def weinbergAngle : ℝ := Real.arccos massRatio
62
63/-- sin²(θ_W) - the key electroweak parameter. -/
64noncomputable def sin2ThetaW : ℝ := 1 - massRatio^2
65
66/-- **THEOREM**: sin²(θ_W) ≈ 0.223. -/
67theorem sin2_theta_w_value : sin2ThetaW > 0.22 ∧ sin2ThetaW < 0.23 := by
68 unfold sin2ThetaW massRatio m_W m_Z
69 constructor <;> norm_num
70
71/-! ## φ-Connection Hypotheses -/
72
73/-- Hypothesis 1: cos(θ_W) = √(1 - 1/φ²)
74
75 √(1 - 1/φ²) = √(1 - 0.382) = √0.618 ≈ 0.786
76
77 This is too small compared to observed 0.881. -/
78noncomputable def hypothesis1 : ℝ := Real.sqrt (1 - 1/phi^2)
79
80/-- Hypothesis 2: cos(θ_W) = (φ + 1) / (φ + 2)
81
82 (1.618 + 1) / (1.618 + 2) = 2.618 / 3.618 ≈ 0.724
83
84 This is also too small. -/
85noncomputable def hypothesis2 : ℝ := (phi + 1) / (phi + 2)
86
87/-- Hypothesis 3: cos(θ_W) = φ / √(φ² + 1)
88
89 1.618 / √(2.618 + 1) = 1.618 / 1.902 ≈ 0.851
90
91 Getting closer! -/