Trace recurrence for iterated unit action
Provedpell_step_recurrencenumber-theorypell-equation
Iterating the unit action once more satisfies the second-order trace recurrence (the Chebyshev shape of PellV/PellW sequences), using only the unit equation.
Preamble
import Mathlib.Tactic
Formal statement
theorem pell_step_recurrence {D u v x0 y0 x1 y1 : Int} (hunit : u ^ 2 - D * v ^ 2 = 1) (hx : x1 = u * x0 + D * v * y0) (hy : y1 = v * x0 + u * y0) : u * x1 + D * v * y1 = 2 * u * x1 - x0 := by sorrySource