phi_inv_eq

formal source

 253/-! ## Negative powers of φ (using φ⁻¹ = φ - 1) -/
 254
 255/-- φ⁻¹ = φ - 1 ≈ 0.618 -/
 256theorem phi_inv_eq : goldenRatio⁻¹ = goldenRatio - 1 := by
 257  -- φ⁻¹ = -ψ = -(1 - √5)/2 = (√5 - 1)/2 = (1 + √5)/2 - 1 = φ - 1
 258  rw [inv_goldenRatio]
 259  unfold goldenRatio goldenConj
 260  ring
 261
 262theorem phi_inv_gt : (0.618 : ℝ) < goldenRatio⁻¹ := by
 263  rw [phi_inv_eq]
 264  have h := phi_gt_1618
 265  linarith
 266
 267theorem phi_inv_lt : goldenRatio⁻¹ < (0.6186 : ℝ) := by
 268  rw [phi_inv_eq]
 269  have h := phi_lt_16185
 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)