`phi_gt_onePointFive`

proved

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Constants on GitHub at line 78.

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

  75  linear_combination (1/4) * hsq
  76
  77/-- Tighter lower bound: φ > 1.5 (since √5 > 2, so (1 + √5)/2 > 1.5). -/
  78lemma phi_gt_onePointFive : (1.5 : ℝ) < phi := by
  79  simp only [phi]
  80  have h5 : (2 : ℝ) < Real.sqrt 5 := by
  81    have h : (2 : ℝ)^2 < 5 := by norm_num
  82    rw [← Real.sqrt_sq (by norm_num : (0 : ℝ) ≤ 2)]
  83    exact Real.sqrt_lt_sqrt (by norm_num) h
  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]

papers checked against this theorem

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