`phi_lt_onePointSixTwo`

proved

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Constants on GitHub at line 87.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

used by

formal source

  84  linarith
  85
  86/-- Tighter upper bound: φ < 1.62 (since √5 < 2.24). -/
  87lemma phi_lt_onePointSixTwo : phi < (1.62 : ℝ) := by
  88  simp only [phi]
  89  have h5 : Real.sqrt 5 < (2.24 : ℝ) := by
  90    have h : (5 : ℝ) < (2.24 : ℝ)^2 := by norm_num
  91    have h24_pos : (0 : ℝ) ≤ 2.24 := by norm_num
  92    rw [← Real.sqrt_sq h24_pos]
  93    exact Real.sqrt_lt_sqrt (by norm_num) h
  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

papers checked against this theorem

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