theorem
proved
tactic proof
deltaCP_prediction_matches
show as:
view Lean formalization →
formal statement (Lean)
195theorem deltaCP_prediction_matches :
196 -- predicted_deltaCP ≈ π + 0.0618π ≈ 191° (in radians: ≈ 3.334)
197 -- observed deltaCP ≈ 197° = 3.438 rad
198 -- The prediction is in a physically reasonable range (between π and 2π)
199 predicted_deltaCP > Real.pi ∧ predicted_deltaCP < 2 * Real.pi := by
proof body
Tactic-mode proof.
200 unfold predicted_deltaCP phi
201 have h_phi_gt_1 := one_lt_phi
202 have h_phi_lt_2 := phi_lt_two
203 have h_pi_pos := Real.pi_pos
204 -- phi = (1 + √5)/2, so phi - 1 = (√5 - 1)/2 > 0 and < 1
205 have h_phi_sub1_pos : (1 + Real.sqrt 5) / 2 - 1 > 0 := by
206 have h := h_phi_gt_1
207 unfold phi at h
208 linarith
209 have h_phi_sub1_lt1 : (1 + Real.sqrt 5) / 2 - 1 < 1 := by
210 have h := h_phi_lt_2
211 unfold phi at h
212 linarith
213 constructor
214 · -- predicted > π because (φ-1) > 0
215 have h : ((1 + Real.sqrt 5) / 2 - 1) * Real.pi / 10 > 0 := by
216 apply div_pos
217 · apply mul_pos h_phi_sub1_pos h_pi_pos
218 · norm_num
219 linarith
220 · -- predicted < 2π because (φ-1) < 1, so predicted < π + π/10 < 2π
221 have h_bound : ((1 + Real.sqrt 5) / 2 - 1) * Real.pi / 10 < Real.pi / 10 := by
222 apply div_lt_div_of_pos_right _ (by norm_num : (0 : ℝ) < 10)
223 calc ((1 + Real.sqrt 5) / 2 - 1) * Real.pi
224 < 1 * Real.pi := by apply mul_lt_mul_of_pos_right h_phi_sub1_lt1 h_pi_pos
225 _ = Real.pi := by ring
226 calc Real.pi + ((1 + Real.sqrt 5) / 2 - 1) * Real.pi / 10
227 < Real.pi + Real.pi / 10 := by linarith
228 _ = 11 / 10 * Real.pi := by ring
229 _ < 2 * Real.pi := by linarith
230
231/-! ## Majorana Phases -/
232
233/-- If neutrinos are Majorana particles, there are two additional phases:
234
235 α₁, α₂ (Majorana phases)
236
237 These don't affect oscillations but matter for neutrinoless double beta decay.
238 RS may predict these from 8-tick constraints. -/