phi_squared_bounds

formal source

  88/-- **CALCULATED**: φ² bounds (useful for many calculations).
  89    
  90    With 1.61 < φ < 1.62: 2.59 < φ² < 2.62 -/
  91theorem phi_squared_bounds : (2.59 : ℝ) < phi^2 ∧ phi^2 < (2.62 : ℝ) := by
  92  have h1 : phi ^ 2 = phi + 1 := phi_sq_eq
  93  rw [h1]
  94  have h2 : phi > (1.61 : ℝ) := phi_gt_onePointSixOne
  95  have h3 : phi < (1.62 : ℝ) := phi_lt_onePointSixTwo
  96  constructor
  97  · nlinarith
  98  · nlinarith
  99
 100/-- **CALCULATED**: φ⁴ = (φ²)² bounds.
 101    
 102    With 2.59 < φ² < 2.62: 6.7 < φ⁴ < 6.9 -/
 103theorem phi_fourth_bounds : (6.7 : ℝ) < (phi : ℝ)^(4 : ℕ) ∧ (phi : ℝ)^(4 : ℕ) < (6.9 : ℝ) := by
 104  have h1 : (phi : ℝ)^(4 : ℕ) = (phi ^ 2) ^ 2 := by ring
 105  rw [h1]
 106  have h2 : (2.59 : ℝ) < phi^2 := phi_squared_bounds.1
 107  have h3 : phi^2 < (2.62 : ℝ) := phi_squared_bounds.2
 108  constructor
 109  · nlinarith
 110  · nlinarith
 111
 112/-- **CALCULATED**: φ⁵ bounds (for BAO scale predictions).
 113    
 114    φ⁵ = φ⁴ × φ, so with 6.7 < φ⁴ < 6.9 and 1.61 < φ < 1.62:
 115    10.7 < φ⁵ < 11.3 -/
 116theorem phi_fifth_bounds : (10.7 : ℝ) < (phi : ℝ)^(5 : ℕ) ∧ (phi : ℝ)^(5 : ℕ) < (11.3 : ℝ) := by
 117  have h1 : (phi : ℝ)^(5 : ℕ) = (phi : ℝ)^(4 : ℕ) * phi := by ring
 118  rw [h1]
 119  have h2 : (6.7 : ℝ) < (phi : ℝ)^(4 : ℕ) := phi_fourth_bounds.1
 120  have h3 : (phi : ℝ)^(4 : ℕ) < (6.9 : ℝ) := phi_fourth_bounds.2
 121  have h4 : phi > (1.61 : ℝ) := phi_gt_onePointSixOne