Exact limit of reciprocal iteration
ProvedWorkbookCorrected.plus_25846corrected-formalizationlean-workbooksequencessource-checked
Let x₁ = 1 and xₙ₊₁ = 1/(1+xₙ) for every integer n ≥ 1. Then xₙ converges to (√5−1)/2.
Formalization Note: Restores the source’s initial index and supplies the exact requested limit with the full epsilon definition of convergence.
Source: InternLM Lean-Workbook, record lean_workbook_plus_25846 (Apache-2.0).
Preamble
import Mathlib
Formal statement
theorem WorkbookCorrected.plus_25846 (x : ℕ → ℝ) (h1 : x 1 = 1)
(h : ∀ n : ℕ, 1 ≤ n → x (n+1) = 1/(1+x n)) :
∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ n : ℕ, N ≤ n →
|x n - (Real.sqrt 5-1)/2| < ε := by sorrySource