Pell's Equation

Statement

For a positive integer $d$ that is not a perfect square, Pell's equation

has infinitely many integer solutions $(x, y)$ with $x, y > 0$. The fundamental solution $(x_1, y_1)$ — the smallest positive one — generates all others via the recurrence

The trivial solution $(1, 0)$ always exists. The interesting content is that a non-trivial solution exists when $d$ is not a perfect square.

Visualization

Solutions to $x^2 - 2y^2 = 1$, generated from the fundamental solution $(3, 2)$:

$n$	$x_n$	$y_n$	$x_n^2 - 2y_n^2$
0	1	0	1
1	3	2	$9 - 8 = 1$
2	17	12	$289 - 288 = 1$
3	99	70	$9801 - 9800 = 1$
4	577	408	$332929 - 332928 = 1$
5	3363	2378	$11309769 - 11309768 = 1$

Each row is produced by $(x_{n+1}, y_{n+1}) = (3x_n + 4y_n,\; 2x_n + 3y_n)$.

Proof Sketch

1. Pigeonhole / continued fractions. Consider the continued fraction expansion of $\sqrt{d}$. Since $d$ is not a square, $\sqrt{d}$ is irrational and its continued fraction is periodic (by Lagrange's theorem).
2. Convergents satisfy the equation. The convergents $p_k/q_k$ of $\sqrt{d}$ satisfy $|p_k - q_k\sqrt{d}| < 1/q_k$. A pigeonhole argument on the fractional parts of $j\sqrt{d}$ for $j = 0, \ldots, \lfloor\sqrt{d}\rfloor + 1$ yields integers $x, y$ with $|x^2 - dy^2| \le 2\sqrt{d}$. Among these, by another pigeonhole step, one value of $x^2 - dy^2$ repeats; subtracting gives a solution to Pell's equation.
3. Infinitely many solutions. If $(x_1, y_1)$ is the fundamental solution, the map $(x, y) \mapsto (x_1 x + d y_1 y,\; x_1 y + y_1 x)$ sends solutions to solutions, producing infinitely many.
4. Group structure. The set of positive solutions forms a free abelian group of rank 1, generated by the fundamental solution.

Connections

Pell's equation is closely connected to Pythagorean TriplesPythagorean Triples$$a = m^2 - n^2,\; b = 2mn,\; c = m^2 + n^2$$Complete parametrisation of all integer solutions to a² + b² = c²Read more →, which arise from a related norm-1 condition over $\mathbb{Z}[i]$. The theory of solutions is an instance of the general theory underlying Quadratic ReciprocityQuadratic Reciprocity$$\left(\frac{p}{q}\right)\left(\frac{q}{p}\right) = (-1)^{\frac{p-1}{2}\cdot\frac{q-1}{2}}$$Relationship between solvability of quadratic congruences for two odd primesRead more →, where quadratic residues determine which primes split in $\mathbb{Z}[\sqrt{d}]$.

import Mathlib.NumberTheory.Pell

/-- The trivial solution (1, 0) always solves x² - dy² = 1. -/
theorem pell_trivial (d : ℕ) : (1 : ℤ)^2 - d * (0 : ℤ)^2 = 1 := by ring

/-- The fundamental solution (3, 2) solves x² - 2y² = 1. -/
theorem pell_3_2 : (3 : ℤ)^2 - 2 * (2 : ℤ)^2 = 1 := by norm_num

/-- For positive non-square d, a nontrivial solution exists.
    Mathlib's `Pell.Solution₁.exists_pos_of_not_isSquare` gives a solution with x > 1, y > 0. -/
theorem pell_exists (d : ℕ) (hd_pos : 0 < d) (hd_sq : ¬IsSquare d) :
    ∃ a : Pell.Solution₁ d, 1 < a.x ∧ 0 < a.y :=
  Pell.Solution₁.exists_pos_of_not_isSquare hd_pos hd_sq