`phi_gt_onePointSixOne`

proved

show as: view math explainer →

module: IndisputableMonolith.Constants
domain: Constants
line: 97 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Constants on GitHub at line 97.

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

  94  linarith
  95
  96/-- Even tighter lower bound: φ > 1.61. -/
  97lemma phi_gt_onePointSixOne : (1.61 : ℝ) < phi := by
  98  simp only [phi]
  99  have h5 : (2.22 : ℝ) < Real.sqrt 5 := by
 100    have h : (2.22 : ℝ)^2 < 5 := by norm_num
 101    rw [← Real.sqrt_sq (by norm_num : (0 : ℝ) ≤ 2.22)]
 102    exact Real.sqrt_lt_sqrt (by norm_num) h
 103  linarith
 104
 105/-- φ² is between 2.5 and 2.7.
 106    φ² = φ + 1 ≈ 2.618 (exact: (3 + √5)/2). -/
 107lemma phi_squared_bounds : (2.5 : ℝ) < phi^2 ∧ phi^2 < 2.7 := by
 108  rw [phi_sq_eq]
 109  have h1 := phi_gt_onePointFive
 110  have h2 := phi_lt_onePointSixTwo
 111  constructor <;> linarith
 112
 113/-! ### Fibonacci power identities for φ -/
 114
 115/-- Key identity: φ³ = 2φ + 1 (Fibonacci recurrence).
 116    φ³ = φ × φ² = φ(φ + 1) = φ² + φ = (φ + 1) + φ = 2φ + 1. -/
 117lemma phi_cubed_eq : phi^3 = 2 * phi + 1 := by
 118  calc phi^3 = phi * phi^2 := by ring
 119    _ = phi * (phi + 1) := by rw [phi_sq_eq]
 120    _ = phi^2 + phi := by ring
 121    _ = (phi + 1) + phi := by rw [phi_sq_eq]
 122    _ = 2 * phi + 1 := by ring
 123
 124/-- Key identity: φ⁴ = 3φ + 2 (Fibonacci recurrence).
 125    φ⁴ = φ × φ³ = φ(2φ + 1) = 2φ² + φ = 2(φ + 1) + φ = 3φ + 2. -/
 126lemma phi_fourth_eq : phi^4 = 3 * phi + 2 := by
 127  calc phi^4 = phi * phi^3 := by ring

papers checked against this theorem

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