def
definition
sin2ThetaW_error
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.StandardModel.WeinbergAngle on GitHub at line 42.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
39noncomputable def sin2ThetaW_observed : ℝ := 0.2229
40
41/-- Uncertainty in sin²(θ_W). -/
42noncomputable def sin2ThetaW_error : ℝ := 0.0003
43
44/-- **THEOREM**: sin²(θ_W) is between 0.22 and 0.23. -/
45theorem sin2_theta_bounds :
46 sin2ThetaW_observed > 0.22 ∧ sin2ThetaW_observed < 0.23 := by
47 unfold sin2ThetaW_observed
48 constructor <;> norm_num
49
50/-! ## φ-Based Predictions -/
51
52/-- **Prediction 1**: sin²(θ_W) = 1/4 - 1/(8φ)
53
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