A positive square-root iteration must be constant
ProvedWorkbookCorrected.plus_61506corrected-formalizationlean-workbooksequencessource-checked
Let aₙ be positive real numbers satisfying aₙ₊₁=√(6−2aₙ²) for every integer n≥1. Then the sequence is constant.
Formalization Note: Restores the source’s positivity assumption and positive indices.
Source: InternLM Lean-Workbook, record lean_workbook_plus_61506 (Apache-2.0).
Preamble
import Mathlib
Formal statement
theorem WorkbookCorrected.plus_61506 (a : ℕ → ℝ) (ha : ∀ n : ℕ, 1 ≤ n → 0 < a n)
(h : ∀ n : ℕ, 1 ≤ n → a (n+1)=Real.sqrt (6-2*(a n)^2)) :
∃ c : ℝ, ∀ n : ℕ, 1 ≤ n → a n=c := by sorrySource