deltaCP_prediction_matches

formal source

 192    This is within 1σ of observations! -/
 193noncomputable def predicted_deltaCP : ℝ := Real.pi + (phi - 1) * Real.pi / 10
 194
 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
 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