phi_pow_neg5_interval

formal source

  72theorem phi_eq_formula : goldenRatio = (1 + Real.sqrt 5) / 2 := rfl
  73
  74/-- φ^(-5) interval ≈ 0.0902 - PROVEN using φ⁻⁵ = (φ⁻¹)⁵ -/
  75def phi_pow_neg5_interval : Interval where
  76  lo := 89 / 1000  -- Matches phi_inv5_interval_proven
  77  hi := 91 / 1000
  78  valid := by norm_num
  79
  80theorem phi_pow_neg5_in_interval : phi_pow_neg5_interval.contains (((1 + Real.sqrt 5) / 2) ^ (-5 : ℝ)) := by
  81  -- φ^(-5) = (φ⁻¹)^5
  82  simp only [Interval.contains, phi_pow_neg5_interval]
  83  rw [← phi_eq_formula]
  84  have hpos : (0 : ℝ) < goldenRatio := Real.goldenRatio_pos
  85  have h : goldenRatio ^ (-5 : ℝ) = goldenRatio⁻¹ ^ 5 := by
  86    rw [Real.rpow_neg (le_of_lt hpos)]
  87    have : (5 : ℝ) = (5 : ℕ) := by norm_num
  88    rw [this, Real.rpow_natCast, inv_pow]
  89  rw [h]
  90  have hcontains := phi_inv5_in_interval_proven
  91  simp only [Interval.contains, phi_inv5_interval_proven] at hcontains
  92  constructor
  93  · have h1 : ((89 / 1000 : ℚ) : ℝ) = (0.089 : ℝ) := by norm_num
  94    linarith [hcontains.1]
  95  · have h1 : ((91 / 1000 : ℚ) : ℝ) = (0.091 : ℝ) := by norm_num
  96    linarith [hcontains.2]
  97
  98/-- φ^(-3) interval ≈ 0.236 - PROVEN using φ⁻³ = (φ⁻¹)³ -/
  99def phi_pow_neg3_interval : Interval where
 100  lo := 2359 / 10000  -- Matches phi_inv3_interval_proven
 101  hi := 237 / 1000
 102  valid := by norm_num
 103
 104theorem phi_pow_neg3_in_interval : phi_pow_neg3_interval.contains (((1 + Real.sqrt 5) / 2) ^ (-3 : ℝ)) := by
 105  simp only [Interval.contains, phi_pow_neg3_interval]