phi_bounds

proof body

Tactic-mode proof.

 293  -- φ = (1 + √5)/2
 294  -- We need: 2.236066 < √5 < 2.236068
 295  have sqrt5_lower : (2.236066 : ℝ) < Real.sqrt 5 := by
 296    have h : (2.236066 : ℝ)^2 < 5 := by norm_num
 297    have h_pos : (0 : ℝ) ≤ 2.236066 := by norm_num
 298    rw [← Real.sqrt_sq h_pos]
 299    exact Real.sqrt_lt_sqrt (by norm_num) h
 300  have sqrt5_upper : Real.sqrt 5 < (2.236068 : ℝ) := by
 301    have h : (5 : ℝ) < (2.236068)^2 := by norm_num
 302    have h_pos : (0 : ℝ) ≤ 2.236068 := by norm_num
 303    rw [← Real.sqrt_sq h_pos]
 304    exact Real.sqrt_lt_sqrt (by positivity) h
 305  constructor
 306  · -- Lower bound
 307    have h : (1.618033 : ℝ) < (1 + Real.sqrt 5) / 2 := by
 308      have : (1 : ℝ) + 2.236066 < 1 + Real.sqrt 5 := by linarith
 309      linarith
 310    simp only [phi]
 311    exact h
 312  · -- Upper bound
 313    have h : (1 + Real.sqrt 5) / 2 < (1.618034 : ℝ) := by
 314      have : (1 : ℝ) + Real.sqrt 5 < 1 + 2.236068 := by linarith
 315      linarith
 316    simp only [phi]
 317    exact h
 318
 319/-- Hypothesis: log(1.618033) > 0.481211 (verified externally via Taylor expansion) -/