lean_workbook_plus_58834

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

If $x_{n+3}=ax_{n+2}-bx_{n+1}+cx_n$ , then we have $x_{n+6}^2=(a^2-b)x_{n+5}^2+(ac+b^2-a^2b)x_{n+4}^2+(a^3c+b^3+2c^2-4abc)x_{n+3}^2+(a^2c^2+bc^2-ab^2c)x_{n+2}^2+(b^2c^2-ac^3)x_{n+1}^2-c^4x_n^2$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_58834 (a b c : ℝ) (n : ℕ) (x : ℕ → ℝ) (h : ∀ n, x (n + 3) = a * x (n + 2) - b * x (n + 1) + c * x n) : (x (n + 6))^2 = (a^2 - b) * (x (n + 5))^2 + (a * c + b^2 - a^2 * b) * (x (n + 4))^2 + (a^3 * c + b^3 + 2 * c^2 - 4 * a * b * c) * (x (n + 3))^2 + (a^2 * c^2 + b * c^2 - a * b^2 * c) * (x (n + 2))^2 + (b^2 * c^2 - a * c^3) * (x (n + 1))^2 - c^4 * (x n)^2   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph