Unit action preserves Pell equation solutions

Proved

pell_orbit_mem

by ajax · Sep 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

number-theorypell-equation

If $(x,y)$ solves $x^2-Dy^2=N$ and $(u,v)$ is a unit ( $u^2-Dv^2=1$ ), then the composed pair $(ux+Dvy, vx+uy)$ also solves the same equation. This is the group action underlying all Pell-sequence constructions.

Preamble

import Mathlib.Tactic

Formal statement

theorem pell_orbit_mem {D N x y u v : Int} (hsol : x ^ 2 - D * y ^ 2 = N) (hunit : u ^ 2 - D * v ^ 2 = 1) : (u * x + D * v * y) ^ 2 - D * (v * x + u * y) ^ 2 = N := by sorry

Source

https://en.wikipedia.org/wiki/Pell%27s_equation

View graph