def
definition
phi_prediction_theta13
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.StandardModel.PMNSMatrix on GitHub at line 104.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
101 sin²θ₁₃ ≈ φ/100 = 0.01618
102
103 Observed ≈ 0.022, within 30%. Not great. -/
104noncomputable def phi_prediction_theta13 : ℝ := phi / 100
105
106/-- **Hypothesis 4: Tribimaximal mixing (TBM) + corrections**
107
108 TBM predicts:
109 - sin²θ₁₂ = 1/3 = 0.333
110 - sin²θ₂₃ = 1/2 = 0.5
111 - sin²θ₁₃ = 0 (wrong!)
112
113 Reality deviates from TBM by φ-corrections. -/
114noncomputable def TBM_theta12 : ℝ := 1 / 3
115noncomputable def TBM_theta23 : ℝ := 1 / 2
116noncomputable def TBM_theta13 : ℝ := 0
117
118/-- **Hypothesis 5: Golden Ratio Mixing (GRM)**
119
120 sin²θ₁₂ = (2 + φ)⁻¹ = 1/3.618 ≈ 0.276
121
122 Or alternatively:
123 sin θ₁₂ = 1/√(1 + φ²) = 0.526
124 sin²θ₁₂ = 0.277
125
126 Still ~10% from observed. -/
127noncomputable def GRM_theta12 : ℝ := 1 / (2 + phi)
128
129/-! ## RS-Corrected Mixing -/
130
131/-- The RS correction to tribimaximal mixing:
132
133 Δ(sin²θ₁₂) = 1/3 - 0.307 = 0.026 ≈ (φ - 1)² = 0.382² ≈ 0.146
134