Integer terms from a consecutive-product square invariant
ProvedWorkbookCorrected.plus_56310corrected-formalizationlean-workbooksequencessource-checked
Let x₁=603, x₂=102, and xₙ₊₂=xₙ₊₁+xₙ+2√(xₙxₙ₊₁−2) for every integer n ≥ 1. Then every term is an integer.
Formalization Note: Restores the source’s initial indices 1 and 2 and its recurrence at positive indices.
Source: InternLM Lean-Workbook, record lean_workbook_plus_56310 (Apache-2.0).
Preamble
import Mathlib
Formal statement
theorem WorkbookCorrected.plus_56310 (x : ℕ → ℝ) (h1 : x 1=603) (h2 : x 2=102)
(h : ∀ n : ℕ, 1 ≤ n → x (n+2)=x (n+1)+x n+2*Real.sqrt (x n*x (n+1)-2)) :
∀ n : ℕ, 1 ≤ n → ∃ k : ℤ, x n=(k:ℝ) := by sorrySource