phiPredictedMR

formal source

  29
  30/-! ## φ-Connection to the Seesaw Scale -/
  31
  32noncomputable def phiPredictedMR : ℝ := (1.2e19) / phi^13
  33
  34/-- Auxiliary lemma for phi^13 using Fibonacci numbers. -/
  35lemma phi_pow13 : phi^13 = 233 * phi + 144 := by
  36  have h2 : phi^2 = phi + 1 := phi_sq_eq
  37  have h3 : phi^3 = 2 * phi + 1 := by rw [pow_succ, h2]; ring_nf; rw [h2]; ring_nf
  38  have h4 : phi^4 = 3 * phi + 2 := by rw [pow_succ, h3]; ring_nf; rw [h2]; ring_nf
  39  have h5 : phi^5 = 5 * phi + 3 := by rw [pow_succ, h4]; ring_nf; rw [h2]; ring_nf
  40  have h6 : phi^6 = 8 * phi + 5 := by rw [pow_succ, h5]; ring_nf; rw [h2]; ring_nf
  41  have h7 : phi^7 = 13 * phi + 8 := by rw [pow_succ, h6]; ring_nf; rw [h2]; ring_nf
  42  have h8 : phi^8 = 21 * phi + 13 := by rw [pow_succ, h7]; ring_nf; rw [h2]; ring_nf
  43  have h9 : phi^9 = 34 * phi + 21 := by rw [pow_succ, h8]; ring_nf; rw [h2]; ring_nf
  44  have h10 : phi^10 = 55 * phi + 34 := by rw [pow_succ, h9]; ring_nf; rw [h2]; ring_nf
  45  have h11 : phi^11 = 89 * phi + 55 := by rw [pow_succ, h10]; ring_nf; rw [h2]; ring_nf
  46  have h12 : phi^12 = 144 * phi + 89 := by rw [pow_succ, h11]; ring_nf; rw [h2]; ring_nf
  47  have h13 : phi^13 = 233 * phi + 144 := by rw [pow_succ, h12]; ring_nf; rw [h2]; ring_nf
  48  exact h13
  49
  50theorem seesaw_scale_phi_connection :
  51    abs (phiPredictedMR - (2.3e16 : ℝ)) < (1e15 : ℝ) := by
  52  unfold phiPredictedMR
  53  -- phi = goldenRatio
  54  have h_phi_eq : phi = goldenRatio := rfl
  55  have hlo : (1.618 : ℝ) < phi := by rw [h_phi_eq]; exact phi_gt_1618
  56  have hhi : phi < (1.6185 : ℝ) := by rw [h_phi_eq]; exact phi_lt_16185
  57  have h13lo : (520 : ℝ) < phi^13 := by
  58    rw [phi_pow13]
  59    have : (520 : ℝ) < 233 * (1.618 : ℝ) + 144 := by norm_num
  60    linarith
  61  have h13hi : phi^13 < (522 : ℝ) := by
  62    rw [phi_pow13]