phi_pow_neg3_interval

formal source

  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]
 106  rw [← phi_eq_formula]
 107  have hpos : (0 : ℝ) < goldenRatio := Real.goldenRatio_pos
 108  have h : goldenRatio ^ (-3 : ℝ) = goldenRatio⁻¹ ^ 3 := by
 109    rw [Real.rpow_neg (le_of_lt hpos)]
 110    have : (3 : ℝ) = (3 : ℕ) := by norm_num
 111    rw [this, Real.rpow_natCast, inv_pow]
 112  rw [h]
 113  have hcontains := phi_inv3_in_interval_proven
 114  simp only [Interval.contains, phi_inv3_interval_proven] at hcontains
 115  constructor
 116  · have h1 : ((2359 / 10000 : ℚ) : ℝ) = (0.2359 : ℝ) := by norm_num
 117    linarith [hcontains.1]
 118  · have h1 : ((237 / 1000 : ℚ) : ℝ) = (0.237 : ℝ) := by norm_num
 119    linarith [hcontains.2]
 120
 121/-- φ^51 interval - using proven bounds from PhiBounds -/
 122def phi_pow_51_interval : Interval where
 123  lo := 45537548334  -- Match phi_pow51_interval_proven
 124  hi := 45537549354
 125  valid := by norm_num
 126
 127theorem phi_pow_51_in_interval :
 128    phi_pow_51_interval.contains (((1 + Real.sqrt 5) / 2) ^ (51 : ℝ)) := by
 129  simp only [Interval.contains, phi_pow_51_interval]