hubble_resolution_converges

proof body

Tactic-mode proof.

  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
  64      have hphi_gt : 1.61 < phi := by
  65        have h5 : (2.23 : ℝ)^2 < 5 := by norm_num
  66        have hsqrt5 : 2.23 < Real.sqrt 5 := by
  67          rw [← Real.sqrt_sq (by norm_num : (0:ℝ) ≤ 2.23)]
  68          exact Real.sqrt_lt_sqrt (by norm_num) h5
  69        unfold phi; linarith
  70      rw [inv_lt₀ (by norm_num) (by linarith)]
  71      linarith
  72
  73  -- Calculation: 67.4 * (1 + [0.09, 0.091]) = [67.4 + 6.066, 67.4 + 6.1334] = [73.466, 73.5334]
  74  -- |[73.466, 73.5334] - 73.5| = |[-0.034, 0.0334]| < 0.5
  75  rw [abs_lt]
  76  constructor
  77  · -- -0.5 < 67.4 * (1 + phi^-5) - 73.5  <=>  73.0 < 67.4 * (1 + phi^-5)
  78    calc (73.0 : ℝ) < 67.4 * (1 + 0.09) := by norm_num
  79      _ < 67.4 * (1 + phi ^ (-(5 : ℝ))) := by gcongr; exact h_phi_pow5_inv.1
  80  · -- 67.4 * (1 + phi^-5) - 73.5 < 0.5  <=>  67.4 * (1 + phi^-5) < 74.0
  81    calc 67.4 * (1 + phi ^ (-(5 : ℝ))) < 67.4 * (1 + 0.091) := by gcongr; exact h_phi_pow5_inv.2
  82      _ < 74.0 := by norm_num
  83
  84/-- **DEFINITION: Sigma-8 Suppression**
  85    Structural growth is suppressed by the recognition strain Q. -/