def
definition
maximal_theta23
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.StandardModel.PMNSMatrix on GitHub at line 97.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
94
95 Observed ≈ 0.545, close to maximal but slightly off.
96 A small φ-correction could explain the deviation. -/
97noncomputable def maximal_theta23 : ℝ := 1 / 2
98
99/-- **Hypothesis 3: θ₁₃ from φ/10**
100
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)