Integrality of a square-root recurrence via a Pell invariant
ProvedWorkbookCorrected.plus_40328corrected-formalizationlean-workbooksequencessource-checked
Let a₁ = 1 and aₙ₊₁ = 2aₙ+√(3aₙ²+1) for every integer n ≥ 1. Every term aₙ is an integer.
Formalization Note: Restores the source’s initial index 1 and its recurrence on positive indices. Equality to the integer floor expresses the stated integrality.
Source: InternLM Lean-Workbook, record lean_workbook_plus_40328 (Apache-2.0).
Preamble
import Mathlib
Formal statement
theorem WorkbookCorrected.plus_40328 (a : ℕ → ℝ) (h1 : a 1=1)
(h : ∀ n : ℕ, 1 ≤ n → a (n+1)=2*a n+Real.sqrt (3*a n^2+1)) :
∀ n : ℕ, 1 ≤ n → a n = (⌊a n⌋ : ℤ) := by sorrySource