def
definition
def or abbrev
logPhiInterval
show as:
view Lean formalization →
formal statement (Lean)
69def logPhiInterval : Interval where
70 lo := 48 / 100
proof body
Definition body.
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 -/