def
definition
prediction3
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 71.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
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
88
89 Predicted: 0.230
90 Observed: 0.2229
91 Error: ~3.2%
92
93 This is the most promising φ-connection! -/
94noncomputable def bestPrediction : ℝ := prediction3
95
96theorem best_prediction_close_to_observed :
97 |bestPrediction - sin2ThetaW_observed| < 0.01 := by
98 unfold bestPrediction prediction3 sin2ThetaW_observed
99 -- Need: |(3 - φ)/6 - 0.2229| < 0.01
100 -- φ > 1.61 → (3 - φ)/6 < 1.39/6 = 0.2317
101 -- φ < 1.62 → (3 - φ)/6 > 1.38/6 = 0.23