phi_inv3_lt

formal source

 424  have hpos2 : 0 < goldenRatio⁻¹ ^ 2 := sq_pos_of_pos hpos
 425  nlinarith [sq_nonneg goldenRatio⁻¹]
 426
 427theorem phi_inv3_lt : goldenRatio⁻¹ ^ 3 < (0.237 : ℝ) := by
 428  have h1 := phi_inv_lt
 429  have h2 := phi_inv2_lt
 430  have hpos : 0 < goldenRatio⁻¹ := inv_pos.mpr goldenRatio_pos
 431  nlinarith [sq_nonneg goldenRatio⁻¹]
 432
 433/-- Interval containing (φ⁻¹)³ - PROVEN -/
 434def phi_inv3_interval_proven : Interval where
 435  lo := 2359 / 10000
 436  hi := 237 / 1000
 437  valid := by norm_num
 438
 439theorem phi_inv3_in_interval_proven : phi_inv3_interval_proven.contains (goldenRatio⁻¹ ^ 3) := by
 440  simp only [Interval.contains, phi_inv3_interval_proven]
 441  constructor
 442  · have h := phi_inv3_gt
 443    exact le_of_lt (by calc ((2359 / 10000 : ℚ) : ℝ) = (0.2359 : ℝ) := by norm_num
 444      _ < goldenRatio⁻¹ ^ 3 := h)
 445  · have h := phi_inv3_lt
 446    exact le_of_lt (by calc goldenRatio⁻¹ ^ 3 < (0.237 : ℝ) := h
 447      _ = ((237 / 1000 : ℚ) : ℝ) := by norm_num)
 448
 449/-! ## Direct bounds for φ^(-3) (zpow form)
 450
 451Some physics modules use `phi ^ (-3 : ℤ)` directly (rather than `(phi⁻¹)^3`), so we provide
 452an explicit, proven envelope in zpow form.
 453
 454This replaces the legacy `Numerics/Interval.lean` theorem `phi_inv3_zpow_bounds`. -/
 455
 456theorem phi_inv3_zpow_bounds :
 457    (0.2360 : ℝ) < goldenRatio ^ (-3 : ℤ) ∧ goldenRatio ^ (-3 : ℤ) < (0.2361 : ℝ) := by