English
The recurrence s(i) has the closed form s(i) = ω^{2^i} + ω_b^{2^i} in X_q.
Русский
Для последовательности s(i) существует замкнутая форма: s(i) = ω^{2^i} + ω_b^{2^i} в X_q.
LaTeX
$$$ (s(i) : X q) = (\omega : X q)^{2^i} + (\omega_b : X q)^{2^i} $$$
Lean4
/-- A closed form for the recurrence relation. -/
theorem closed_form (i : ℕ) : (s i : X q) = (ω : X q) ^ 2 ^ i + (ωb : X q) ^ 2 ^ i := by
induction i with
| zero =>
dsimp [s, ω, ωb]
ext <;> norm_num
| succ i ih =>
calc
(s (i + 1) : X q) = (s i ^ 2 - 2 : ℤ) := rfl
_ = (s i : X q) ^ 2 - 2 := by push_cast; rfl
_ = (ω ^ 2 ^ i + ωb ^ 2 ^ i) ^ 2 - 2 := by rw [ih]
_ = (ω ^ 2 ^ i) ^ 2 + (ωb ^ 2 ^ i) ^ 2 + 2 * (ωb ^ 2 ^ i * ω ^ 2 ^ i) - 2 := by ring
_ = (ω ^ 2 ^ i) ^ 2 + (ωb ^ 2 ^ i) ^ 2 := by rw [← mul_pow ωb ω, ωb_mul_ω, one_pow, mul_one, add_sub_cancel_right]
_ = ω ^ 2 ^ (i + 1) + ωb ^ 2 ^ (i + 1) := by rw [← pow_mul, ← pow_mul, _root_.pow_succ]
