phi_bounds

formal source

 289-/
 290
 291/-- φ is bounded: φ ∈ (1.618033, 1.618034) -/
 292lemma phi_bounds : (1.618033 : ℝ) < phi ∧ phi < (1.618034 : ℝ) := by
 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) -/
 320def log_lower_bound_phi_hypothesis : Prop := (0.481211 : ℝ) < Real.log (1.618033 : ℝ)
 321
 322/-- Hypothesis: log(1.618034) < 0.481213 (verified externally via Taylor expansion) -/