def
definition
prediction1
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.StandardModel.WeinbergAngle on GitHub at line 57.
browse module
All declarations in this module, on Recognition.
explainer page
formal source
54 = 0.25 - 0.0773 = 0.1727
55
56 Too small. -/
57noncomputable def prediction1 : ℝ := 1/4 - 1/(8*phi)
58
59/-- **Prediction 2**: sin²(θ_W) = 1 - φ/2
60
61 = 1 - 0.809 = 0.191
62
63 Close but still small. -/
64noncomputable def prediction2 : ℝ := 1 - phi/2
65
66/-- **Prediction 3**: sin²(θ_W) = (3 - φ) / 6
67
68 = (3 - 1.618) / 6 = 1.382 / 6 = 0.230
69
70 Very close! Error: ~3% -/
71noncomputable def prediction3 : ℝ := (3 - phi) / 6
72
73/-- **Prediction 4**: sin²(θ_W) = 1 - 3/(4φ)
74
75 = 1 - 0.464 = 0.536
76
77 Too large. -/
78noncomputable def prediction4 : ℝ := 1 - 3/(4*phi)
79
80/-- **Prediction 5**: sin²(θ_W) = (φ - 1)² / 2
81
82 = 0.618² / 2 = 0.382 / 2 = 0.191
83
84 Same as prediction 2. -/
85noncomputable def prediction5 : ℝ := (phi - 1)^2 / 2
86
87/-- **BEST FIT**: sin²(θ_W) = (3 - φ) / 6