phi_inv_interval_proven

formal source

 270  linarith
 271
 272/-- Interval containing φ⁻¹ - PROVEN -/
 273def phi_inv_interval_proven : Interval where
 274  lo := 618 / 1000
 275  hi := 6186 / 10000
 276  valid := by norm_num
 277
 278theorem phi_inv_in_interval_proven : phi_inv_interval_proven.contains goldenRatio⁻¹ := by
 279  simp only [Interval.contains, phi_inv_interval_proven]
 280  constructor
 281  · have h := phi_inv_gt
 282    exact le_of_lt (by calc ((618 / 1000 : ℚ) : ℝ) = (0.618 : ℝ) := by norm_num
 283      _ < goldenRatio⁻¹ := h)
 284  · have h := phi_inv_lt
 285    exact le_of_lt (by calc goldenRatio⁻¹ < (0.6186 : ℝ) := h
 286      _ = ((6186 / 10000 : ℚ) : ℝ) := by norm_num)
 287
 288/-! ## Higher powers using Fibonacci recurrence φ^(n+2) = φ^(n+1) + φ^n -/
 289
 290/-- φ³ = φ² + φ = (φ + 1) + φ = 2φ + 1 -/
 291theorem phi_cubed_eq : goldenRatio ^ 3 = 2 * goldenRatio + 1 := by
 292  have h : goldenRatio ^ 2 = goldenRatio + 1 := goldenRatio_sq
 293  calc goldenRatio ^ 3 = goldenRatio ^ 2 * goldenRatio := by ring
 294    _ = (goldenRatio + 1) * goldenRatio := by rw [h]
 295    _ = goldenRatio ^ 2 + goldenRatio := by ring
 296    _ = (goldenRatio + 1) + goldenRatio := by rw [h]
 297    _ = 2 * goldenRatio + 1 := by ring
 298
 299theorem phi_cubed_gt : (4.236 : ℝ) < goldenRatio ^ 3 := by
 300  rw [phi_cubed_eq]
 301  have h := phi_gt_1618
 302  linarith
 303