`phi_inv_gt`

proved

show as: view math explainer →

module: IndisputableMonolith.Numerics.Interval.PhiBounds
domain: Numerics
line: 262 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Numerics.Interval.PhiBounds on GitHub at line 262.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 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)
 287
 288/-! ## Higher powers using Fibonacci recurrence φ^(n+2) = φ^(n+1) + φ^n -/
 289
 290/-- φ³ = φ² + φ = (φ + 1) + φ = 2φ + 1 -/
 291theorem phi_cubed_eq : goldenRatio ^ 3 = 2 * goldenRatio + 1 := by
 292  have h : goldenRatio ^ 2 = goldenRatio + 1 := goldenRatio_sq

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.