phi_in_phiInterval

formal source

  53  valid := by norm_num
  54
  55/-- φ is in phiInterval - PROVEN using sqrt bounds -/
  56theorem phi_in_phiInterval : phiInterval.contains ((1 + Real.sqrt 5) / 2) := by
  57  simp only [Interval.contains, phiInterval]
  58  constructor
  59  · have h := phi_gt_1618
  60    have h1 : ((1618 / 1000 : ℚ) : ℝ) < (1 + Real.sqrt 5) / 2 := by
  61      calc ((1618 / 1000 : ℚ) : ℝ) = (1.618 : ℝ) := by norm_num
  62        _ < (1 + Real.sqrt 5) / 2 := h
  63    exact le_of_lt h1
  64  · have h := phi_lt_16185
  65    have h1 : (1 + Real.sqrt 5) / 2 < ((1619 / 1000 : ℚ) : ℝ) := by
  66      calc (1 + Real.sqrt 5) / 2 < (1.6185 : ℝ) := h
  67        _ < (1.619 : ℝ) := by norm_num
  68        _ = ((1619 / 1000 : ℚ) : ℝ) := by norm_num
  69    exact le_of_lt h1
  70
  71/-- φ = (1 + √5)/2 (Mathlib definition) -/
  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)]