logPhiInterval

formal source

  66/-- Interval containing log(φ) where φ = (1 + √5)/2 ≈ 1.618
  67    We know log(φ) ≈ 0.4812
  68    Using [0.48, 0.483] to enable proof with 15 Taylor terms -/
  69def logPhiInterval : Interval where
  70  lo := 48 / 100
  71  hi := 483 / 1000
  72  valid := by norm_num
  73
  74/-!
  75## Proving log(φ) bounds using Taylor series
  76
  77We use the identity log(φ) = log(1 + (φ - 1)) and the Taylor series error bound.
  78
  79The Taylor polynomial for log(1+x) up to degree n is:
  80  T_n(x) = x - x²/2 + x³/3 - ... + (-1)^(n+1) * x^n / n
  81
  82The error |log(1+x) - T_n(x)| ≤ |x|^(n+1) / ((n+1)(1-|x|)) for |x| < 1.
  83
  84For x = φ - 1 ≈ 0.618:
  85- We compute T_8(x) using rational bounds
  86- The error is bounded by (0.619)^9 / (9 * (1 - 0.619)) ≈ 0.0025
  87
  88Strategy: Use Complex.norm_log_sub_logTaylor_le from Mathlib, specialized to real numbers.
  89-/
  90
  91/-- For x = φ - 1, we have 0 < x < 1, so |x| = x -/
  92lemma phi_minus_one_abs : |Real.goldenRatio - 1| = Real.goldenRatio - 1 := by
  93  rw [abs_of_pos phi_sub_one_pos]
  94
  95/-- x = φ - 1 satisfies |x| < 1 -/
  96lemma phi_minus_one_abs_lt_one : |Real.goldenRatio - 1| < 1 := by
  97  rw [phi_minus_one_abs]
  98  exact phi_sub_one_lt_one
  99