Boundedness of a quadratic recurrence below its critical initial value

Proved

WorkbookCorrected.base_56341

by wamlart · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

corrected-formalizationlean-workbooksource-checked

Let $0<x_1<1$ and, for every integer $n\ge1$ , define

x_{n+1}=x_n+\frac{x_n^2}{n^2}.

Then there exists a real number $M$ such that $x_n<M$ for every $n\ge1$ .

Formalization Note: The original source formalization incorrectly assumed that every term was already between zero and one. This correction uses only the source initial condition and recurrence and proves boundedness. The sequence is indexed from1 as in the source.

Source: InternLM Lean-Workbook, record lean_workbook_56341 (Apache-2.0).

Preamble

import Mathlib

Formal statement

theorem WorkbookCorrected.base_56341 : ∀ (x : ℕ → ℝ) (h0 : 0 < x 1) (h1 : x 1 < 1)
    (hrec : ∀ n : ℕ, 1 ≤ n → x (n+1) = x n + (x n)^2/(n:ℝ)^2),
    ∃ M : ℝ, ∀ n : ℕ, 1 ≤ n → x n < M := by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_56341; Apache-2.0

View graph