def
definition
def or abbrev
GRM_theta12
show as:
view Lean formalization →
formal statement (Lean)
127noncomputable def GRM_theta12 : ℝ := 1 / (2 + phi)
proof body
Definition body.
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
135 Too large. Try:
136 Δ(sin²θ₁₂) ≈ (φ - 1)³ ≈ 0.236 × 0.382 ≈ 0.090
137
138 Still too large. The correction is subtle. -/