phi_inv5_lt

formal source

 498  have h : goldenRatio⁻¹ ^ 5 = goldenRatio⁻¹ ^ 2 * goldenRatio⁻¹ ^ 3 := by ring
 499  nlinarith
 500
 501theorem phi_inv5_lt : goldenRatio⁻¹ ^ 5 < (0.091 : ℝ) := by
 502  have h2 := phi_inv2_lt
 503  have h3 := phi_inv3_lt
 504  have hpos : 0 < goldenRatio⁻¹ := inv_pos.mpr goldenRatio_pos
 505  have hpos2 : 0 < goldenRatio⁻¹ ^ 2 := sq_pos_of_pos hpos
 506  have hpos3 : 0 < goldenRatio⁻¹ ^ 3 := pow_pos hpos 3
 507  have h : goldenRatio⁻¹ ^ 5 = goldenRatio⁻¹ ^ 2 * goldenRatio⁻¹ ^ 3 := by ring
 508  nlinarith
 509
 510/-- Interval containing (φ⁻¹)⁵ - PROVEN -/
 511def phi_inv5_interval_proven : Interval where
 512  lo := 89 / 1000
 513  hi := 91 / 1000
 514  valid := by norm_num
 515
 516theorem phi_inv5_in_interval_proven : phi_inv5_interval_proven.contains (goldenRatio⁻¹ ^ 5) := by
 517  simp only [Interval.contains, phi_inv5_interval_proven]
 518  constructor
 519  · have h := phi_inv5_gt
 520    exact le_of_lt (by calc ((89 / 1000 : ℚ) : ℝ) = (0.089 : ℝ) := by norm_num
 521      _ < goldenRatio⁻¹ ^ 5 := h)
 522  · have h := phi_inv5_lt
 523    exact le_of_lt (by calc goldenRatio⁻¹ ^ 5 < (0.091 : ℝ) := h
 524      _ = ((91 / 1000 : ℚ) : ℝ) := by norm_num)
 525
 526/-! ## Higher powers for φ^16 -/
 527
 528/-- φ^16 = F₁₆·φ + F₁₅ = 987φ + 610 -/
 529theorem phi_pow16_eq : goldenRatio ^ 16 = 987 * goldenRatio + 610 := by
 530  have h2 : goldenRatio ^ 2 = goldenRatio + 1 := goldenRatio_sq
 531  have h8 : goldenRatio ^ 8 = 21 * goldenRatio + 13 := phi_pow8_eq