Limit of a quadratic iteration with a rational error bound
ProvedWorkbookCorrected.plus_37111corrected-formalizationlean-workbooksequencessource-checked
Let A₁ = 1/2 and Aₙ₊₁ = (Aₙ²+1)/2 for every integer n ≥ 1. Then Aₙ converges to 1.
Formalization Note: Restores the positive recurrence index and the complete epsilon/eventual quantifiers for convergence; the original formalization required arbitrary accuracy at a single index.
Source: InternLM Lean-Workbook, record lean_workbook_plus_37111 (Apache-2.0).
Preamble
import Mathlib
Formal statement
theorem WorkbookCorrected.plus_37111 (a : ℕ → ℝ) (h1 : a 1=1/2)
(h : ∀ n : ℕ, 1 ≤ n → a (n+1)=(a n^2+1)/2) :
∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ n : ℕ, N ≤ n → |a n-1| < ε := by sorrySource