hubble_resolution_converges

formal source

  30
  31    Prediction: H_late = H_early * (1 + phi^-5)
  32    Calculated: 67.4 * (1 + 0.090) = 73.47 -/
  33theorem hubble_resolution_converges :
  34    let H_early : ℝ := 67.4
  35    let H_late_obs : ℝ := 73.5
  36    abs (HubbleParameterILG H_early - H_late_obs) < 0.5 := by
  37  let H_early : ℝ := 67.4
  38  let H_late_obs : ℝ := 73.5
  39  unfold HubbleParameterILG
  40  simp only [cLagLock]
  41  -- phi^-5 is approx 0.09017
  42  have h_phi_pow5_inv : (0.09 : ℝ) < phi ^ (-(5 : ℝ)) ∧ phi ^ (-(5 : ℝ)) < 0.091 := by
  43    -- phi^5 = 5phi + 3. phi in (1.618, 1.619)
  44    -- 5(1.618) + 3 = 8.09 + 3 = 11.09
  45    -- 1 / 11.09 approx 0.09017
  46    have h_phi_fi : phi ^ 5 = 5 * phi + 3 := by
  47      have h_phi_sq : phi ^ 2 = phi + 1 := phi_sq_eq
  48      have h_phi_cu : phi ^ 3 = 2 * phi + 1 := by ring_nf; rw [h_phi_sq]; ring
  49      have h_phi_qu : phi ^ 4 = 3 * phi + 2 := by ring_nf; rw [h_phi_cu, h_phi_sq]; ring
  50      calc phi ^ 5 = phi * phi ^ 4 := by ring
  51        _ = phi * (3 * phi + 2) := by rw [h_phi_qu]
  52        _ = 3 * phi ^ 2 + 2 * phi := by ring
  53        _ = 3 * (phi + 1) + 2 * phi := by rw [h_phi_sq]
  54        _ = 5 * phi + 3 := by ring
  55    rw [Real.rpow_neg phi_pos.le, Real.rpow_natCast, h_phi_fi]
  56    constructor
  57    · -- 0.09 < 1 / (5phi + 3) <=> 5phi + 3 < 1 / 0.09 = 11.111...
  58      -- 5phi < 8.111... <=> phi < 1.622
  59      have hphi_lt : phi < 1.62 := phi_lt_onePointSixTwo
  60      rw [lt_inv₀ (by linarith) (by norm_num)]
  61      linarith
  62    · -- 1 / (5phi + 3) < 0.091 <=> 1 / 0.091 < 5phi + 3
  63      -- 10.989 < 5phi + 3 <=> 7.989 < 5phi <=> 1.597... < phi