Pell's Equation

Pell's Equation is the equation $x^2 - d y^2 = 1$, where $d$ is a positive integer that is not a square, and one is interested in solutions in integers $x$ and $y$.

In this file, we aim at providing all of the essential theory of Pell's Equation for general $d$ (as opposed to the contents of NumberTheory.PellMatiyasevic, which is specific to the case $d = a^2 - 1$ for some $a > 1$).

We begin by defining a type Pell.Solution₁ d for solutions of the equation, show that it has a natural structure as an abelian group, and prove some basic properties.

We then prove the following

Theorem. Let $d$ be a positive integer that is not a square. Then the equation $x^2 - d y^2 = 1$ has a nontrivial (i.e., with $y \ne 0$) solution in integers.

See Pell.exists_of_not_isSquare and Pell.Solution₁.exists_nontrivial_of_not_isSquare.

We then define the fundamental solution to be the solution with smallest $x$ among all solutions satisfying $x > 1$ and $y > 0$. We show that every solution is a power (in the sense of the group structure mentioned above) of the fundamental solution up to a (common) sign, see Pell.IsFundamental.eq_zpow_or_neg_zpow, and that a (positive) solution has this property if and only if it is fundamental, see Pell.pos_generator_iff_fundamental.

References

• K. Ireland, M. Rosen, A classical introduction to modern number theory (Section 17.5)

Tags

Pell's equation

TODO

• Extend to x ^ 2 - d * y ^ 2 = -1 and further generalizations.
• Connect solutions to the continued fraction expansion of √d.

Group structure of the solution set

We define a structure of a commutative multiplicative group with distributive negation on the set of all solutions to the Pell equation x^2 - d*y^2 = 1.

The type of such solutions is Pell.Solution₁ d. It corresponds to a pair of integers x and y and a proof that (x, y) is indeed a solution.

The multiplication is given by (x, y) * (x', y') = (x*y' + d*y*y', x*y' + y*x'). This is obtained by mapping (x, y) to x + y*√d and multiplying the results. In fact, we define Pell.Solution₁ d to be ↥(unitary (ℤ√d)) and transport the "commutative group with distributive negation" structure from ↥(unitary (ℤ√d)).

We then set up an API for Pell.Solution₁ d.

theorem Pell.is_pell_solution_iff_mem_unitary {d : Int} {a : Zsqrtd d} : Iff (Eq (HSub.hSub (HPow.hPow a.re 2) (HMul.hMul d (HPow.hPow a.im 2))) 1) (Membership.mem (unitary (Zsqrtd d)) a)

An element of ℤ√d has norm one (i.e., a.re^2 - d*a.im^2 = 1) if and only if it is contained in the submonoid of unitary elements.

TODO: merge this result with Pell.isPell_iff_mem_unitary.

def Pell.Solution₁ (d : Int) : Type

Pell.Solution₁ d is the type of solutions to the Pell equation x^2 - d*y^2 = 1. We define this in terms of elements of ℤ√d of norm one.

Equations

• Eq (Pell.Solution₁ d) (Subtype fun (x : Zsqrtd d) => Membership.mem (unitary (Zsqrtd d)) x)

def Pell.Solution₁.instCommGroup {d : Int} : CommGroup (Solution₁ d)

Equations

• Eq Pell.Solution₁.instCommGroup (inferInstanceAs (CommGroup (Subtype fun (x : Zsqrtd d) => Membership.mem (unitary (Zsqrtd d)) x)))

def Pell.Solution₁.instHasDistribNeg {d : Int} : HasDistribNeg (Solution₁ d)

Equations

• Eq Pell.Solution₁.instHasDistribNeg (inferInstanceAs (HasDistribNeg (Subtype fun (x : Zsqrtd d) => Membership.mem (unitary (Zsqrtd d)) x)))

def Pell.Solution₁.instInhabited {d : Int} : Inhabited (Solution₁ d)

Equations

• Eq Pell.Solution₁.instInhabited (inferInstanceAs (Inhabited (Subtype fun (x : Zsqrtd d) => Membership.mem (unitary (Zsqrtd d)) x)))

def Pell.Solution₁.instCoeZsqrtd {d : Int} : Coe (Solution₁ d) (Zsqrtd d)

Equations

• Eq Pell.Solution₁.instCoeZsqrtd { coe := Subtype.val }

def Pell.Solution₁.x {d : Int} (a : Solution₁ d) : Int

The x component of a solution to the Pell equation x^2 - d*y^2 = 1

Equations

• Eq a.x a.val.re

def Pell.Solution₁.y {d : Int} (a : Solution₁ d) : Int

The y component of a solution to the Pell equation x^2 - d*y^2 = 1

Equations

• Eq a.y a.val.im

theorem Pell.Solution₁.prop {d : Int} (a : Solution₁ d) : Eq (HSub.hSub (HPow.hPow a.x 2) (HMul.hMul d (HPow.hPow a.y 2))) 1

The proof that a is a solution to the Pell equation x^2 - d*y^2 = 1

theorem Pell.Solution₁.prop_x {d : Int} (a : Solution₁ d) : Eq (HPow.hPow a.x 2) (HAdd.hAdd 1 (HMul.hMul d (HPow.hPow a.y 2)))

An alternative form of the equation, suitable for rewriting x^2.

theorem Pell.Solution₁.prop_y {d : Int} (a : Solution₁ d) : Eq (HMul.hMul d (HPow.hPow a.y 2)) (HSub.hSub (HPow.hPow a.x 2) 1)

An alternative form of the equation, suitable for rewriting d * y^2.

theorem Pell.Solution₁.ext {d : Int} {a b : Solution₁ d} (hx : Eq a.x b.x) (hy : Eq a.y b.y) : Eq a b

Two solutions are equal if their x and y components are equal.

theorem Pell.Solution₁.ext_iff {d : Int} {a b : Solution₁ d} : Iff (Eq a b) (And (Eq a.x b.x) (Eq a.y b.y))

def Pell.Solution₁.mk {d : Int} (x y : Int) (prop : Eq (HSub.hSub (HPow.hPow x 2) (HMul.hMul d (HPow.hPow y 2))) 1) : Solution₁ d

Construct a solution from x, y and a proof that the equation is satisfied.

Equations

• Eq (Pell.Solution₁.mk x y prop) ⟨{ re := x, im := y }, ⋯⟩

theorem Pell.Solution₁.x_mk {d : Int} (x y : Int) (prop : Eq (HSub.hSub (HPow.hPow x 2) (HMul.hMul d (HPow.hPow y 2))) 1) : Eq (mk x y prop).x x

theorem Pell.Solution₁.y_mk {d : Int} (x y : Int) (prop : Eq (HSub.hSub (HPow.hPow x 2) (HMul.hMul d (HPow.hPow y 2))) 1) : Eq (mk x y prop).y y

theorem Pell.Solution₁.coe_mk {d : Int} (x y : Int) (prop : Eq (HSub.hSub (HPow.hPow x 2) (HMul.hMul d (HPow.hPow y 2))) 1) : Eq (mk x y prop).val { re := x, im := y }

theorem Pell.Solution₁.x_one {d : Int} : Eq (Solution₁.x 1) 1

theorem Pell.Solution₁.y_one {d : Int} : Eq (Solution₁.y 1) 0

theorem Pell.Solution₁.x_mul {d : Int} (a b : Solution₁ d) : Eq (HMul.hMul a b).x (HAdd.hAdd (HMul.hMul a.x b.x) (HMul.hMul d (HMul.hMul a.y b.y)))

theorem Pell.Solution₁.y_mul {d : Int} (a b : Solution₁ d) : Eq (HMul.hMul a b).y (HAdd.hAdd (HMul.hMul a.x b.y) (HMul.hMul a.y b.x))

theorem Pell.Solution₁.x_inv {d : Int} (a : Solution₁ d) : Eq (Inv.inv a).x a.x

theorem Pell.Solution₁.y_inv {d : Int} (a : Solution₁ d) : Eq (Inv.inv a).y (Neg.neg a.y)

theorem Pell.Solution₁.x_neg {d : Int} (a : Solution₁ d) : Eq (Neg.neg a).x (Neg.neg a.x)

theorem Pell.Solution₁.y_neg {d : Int} (a : Solution₁ d) : Eq (Neg.neg a).y (Neg.neg a.y)

theorem Pell.Solution₁.eq_zero_of_d_neg {d : Int} (h₀ : LT.lt d 0) (a : Solution₁ d) : Or (Eq a.x 0) (Eq a.y 0)

When d is negative, then x or y must be zero in a solution.

theorem Pell.Solution₁.x_ne_zero {d : Int} (h₀ : LE.le 0 d) (a : Solution₁ d) : Ne a.x 0

A solution has x ≠ 0.

theorem Pell.Solution₁.y_ne_zero_of_one_lt_x {d : Int} {a : Solution₁ d} (ha : LT.lt 1 a.x) : Ne a.y 0

A solution with x > 1 must have y ≠ 0.

theorem Pell.Solution₁.d_pos_of_one_lt_x {d : Int} {a : Solution₁ d} (ha : LT.lt 1 a.x) : LT.lt 0 d

If a solution has x > 1, then d is positive.

theorem Pell.Solution₁.d_nonsquare_of_one_lt_x {d : Int} {a : Solution₁ d} (ha : LT.lt 1 a.x) : Not (IsSquare d)

If a solution has x > 1, then d is not a square.

theorem Pell.Solution₁.eq_one_of_x_eq_one {d : Int} (h₀ : Ne d 0) {a : Solution₁ d} (ha : Eq a.x 1) : Eq a 1

A solution with x = 1 is trivial.

theorem Pell.Solution₁.eq_one_or_neg_one_iff_y_eq_zero {d : Int} {a : Solution₁ d} : Iff (Or (Eq a 1) (Eq a (-1))) (Eq a.y 0)

A solution is 1 or -1 if and only if y = 0.

theorem Pell.Solution₁.x_mul_pos {d : Int} {a b : Solution₁ d} (ha : LT.lt 0 a.x) (hb : LT.lt 0 b.x) : LT.lt 0 (HMul.hMul a b).x

The set of solutions with x > 0 is closed under multiplication.

theorem Pell.Solution₁.y_mul_pos {d : Int} {a b : Solution₁ d} (hax : LT.lt 0 a.x) (hay : LT.lt 0 a.y) (hbx : LT.lt 0 b.x) (hby : LT.lt 0 b.y) : LT.lt 0 (HMul.hMul a b).y

The set of solutions with x and y positive is closed under multiplication.

theorem Pell.Solution₁.x_pow_pos {d : Int} {a : Solution₁ d} (hax : LT.lt 0 a.x) (n : Nat) : LT.lt 0 (HPow.hPow a n).x

If (x, y) is a solution with x positive, then all its powers with natural exponents have positive x.

theorem Pell.Solution₁.y_pow_succ_pos {d : Int} {a : Solution₁ d} (hax : LT.lt 0 a.x) (hay : LT.lt 0 a.y) (n : Nat) : LT.lt 0 (HPow.hPow a n.succ).y

If (x, y) is a solution with x and y positive, then all its powers with positive natural exponents have positive y.

theorem Pell.Solution₁.y_zpow_pos {d : Int} {a : Solution₁ d} (hax : LT.lt 0 a.x) (hay : LT.lt 0 a.y) {n : Int} (hn : LT.lt 0 n) : LT.lt 0 (HPow.hPow a n).y

If (x, y) is a solution with x and y positive, then all its powers with positive exponents have positive y.

theorem Pell.Solution₁.x_zpow_pos {d : Int} {a : Solution₁ d} (hax : LT.lt 0 a.x) (n : Int) : LT.lt 0 (HPow.hPow a n).x

If (x, y) is a solution with x positive, then all its powers have positive x.

theorem Pell.Solution₁.sign_y_zpow_eq_sign_of_x_pos_of_y_pos {d : Int} {a : Solution₁ d} (hax : LT.lt 0 a.x) (hay : LT.lt 0 a.y) (n : Int) : Eq (HPow.hPow a n).y.sign n.sign

If (x, y) is a solution with x and y positive, then the y component of any power has the same sign as the exponent.

theorem Pell.Solution₁.exists_pos_variant {d : Int} (h₀ : LT.lt 0 d) (a : Solution₁ d) : Exists fun (b : Solution₁ d) => And (LT.lt 0 b.x) (And (LE.le 0 b.y) (Membership.mem (Insert.insert b (Insert.insert (Inv.inv b) (Insert.insert (Neg.neg b) (Singleton.singleton (Neg.neg (Inv.inv b)))))) a))

If a is any solution, then one of a, a⁻¹, -a, -a⁻¹ has positive x and nonnegative y.

Existence of nontrivial solutions

theorem Pell.exists_of_not_isSquare {d : Int} (h₀ : LT.lt 0 d) (hd : Not (IsSquare d)) : Exists fun (x : Int) => Exists fun (y : Int) => And (Eq (HSub.hSub (HPow.hPow x 2) (HMul.hMul d (HPow.hPow y 2))) 1) (Ne y 0)

If d is a positive integer that is not a square, then there is a nontrivial solution to the Pell equation x^2 - d*y^2 = 1.

theorem Pell.exists_iff_not_isSquare {d : Int} (h₀ : LT.lt 0 d) : Iff (Exists fun (x : Int) => Exists fun (y : Int) => And (Eq (HSub.hSub (HPow.hPow x 2) (HMul.hMul d (HPow.hPow y 2))) 1) (Ne y 0)) (Not (IsSquare d))

If d is a positive integer, then there is a nontrivial solution to the Pell equation x^2 - d*y^2 = 1 if and only if d is not a square.

theorem Pell.Solution₁.exists_nontrivial_of_not_isSquare {d : Int} (h₀ : LT.lt 0 d) (hd : Not (IsSquare d)) : Exists fun (a : Solution₁ d) => And (Ne a 1) (Ne a (-1))

If d is a positive integer that is not a square, then there exists a nontrivial solution to the Pell equation x^2 - d*y^2 = 1.

theorem Pell.Solution₁.exists_pos_of_not_isSquare {d : Int} (h₀ : LT.lt 0 d) (hd : Not (IsSquare d)) : Exists fun (a : Solution₁ d) => And (LT.lt 1 a.x) (LT.lt 0 a.y)

If d is a positive integer that is not a square, then there exists a solution to the Pell equation x^2 - d*y^2 = 1 with x > 1 and y > 0.

Fundamental solutions

We define the notion of a fundamental solution of Pell's equation and show that it exists and is unique (when d is positive and non-square) and generates the group of solutions up to sign.

def Pell.IsFundamental {d : Int} (a : Solution₁ d) : Prop

We define a solution to be fundamental if it has x > 1 and y > 0 and its x is the smallest possible among solutions with x > 1.

Equations

• Eq (Pell.IsFundamental a) (And (LT.lt 1 a.x) (And (LT.lt 0 a.y) (∀ {b : Pell.Solution₁ d}, LT.lt 1 b.x → LE.le a.x b.x)))

theorem Pell.IsFundamental.x_pos {d : Int} {a : Solution₁ d} (h : IsFundamental a) : LT.lt 0 a.x

A fundamental solution has positive x.

theorem Pell.IsFundamental.d_pos {d : Int} {a : Solution₁ d} (h : IsFundamental a) : LT.lt 0 d

If a fundamental solution exists, then d must be positive.

theorem Pell.IsFundamental.d_nonsquare {d : Int} {a : Solution₁ d} (h : IsFundamental a) : Not (IsSquare d)

If a fundamental solution exists, then d must be a non-square.

theorem Pell.IsFundamental.subsingleton {d : Int} {a b : Solution₁ d} (ha : IsFundamental a) (hb : IsFundamental b) : Eq a b

If there is a fundamental solution, it is unique.

theorem Pell.IsFundamental.exists_of_not_isSquare {d : Int} (h₀ : LT.lt 0 d) (hd : Not (IsSquare d)) : Exists fun (a : Solution₁ d) => IsFundamental a

If d is positive and not a square, then a fundamental solution exists.

theorem Pell.IsFundamental.y_strictMono {d : Int} {a : Solution₁ d} (h : IsFundamental a) : StrictMono fun (n : Int) => (HPow.hPow a n).y

The map sending an integer n to the y-coordinate of a^n for a fundamental solution a is stritcly increasing.

theorem Pell.IsFundamental.zpow_y_lt_iff_lt {d : Int} {a : Solution₁ d} (h : IsFundamental a) (m n : Int) : Iff (LT.lt (HPow.hPow a m).y (HPow.hPow a n).y) (LT.lt m n)

If a is a fundamental solution, then (a^m).y < (a^n).y if and only if m < n.

theorem Pell.IsFundamental.zpow_eq_one_iff {d : Int} {a : Solution₁ d} (h : IsFundamental a) (n : Int) : Iff (Eq (HPow.hPow a n) 1) (Eq n 0)

The nth power of a fundamental solution is trivial if and only if n = 0.

theorem Pell.IsFundamental.zpow_ne_neg_zpow {d : Int} {a : Solution₁ d} (h : IsFundamental a) {n n' : Int} : Ne (HPow.hPow a n) (Neg.neg (HPow.hPow a n'))

A power of a fundamental solution is never equal to the negative of a power of this fundamental solution.

theorem Pell.IsFundamental.x_le_x {d : Int} {a₁ : Solution₁ d} (h : IsFundamental a₁) {a : Solution₁ d} (hax : LT.lt 1 a.x) : LE.le a₁.x a.x

The x-coordinate of a fundamental solution is a lower bound for the x-coordinate of any positive solution.

theorem Pell.IsFundamental.y_le_y {d : Int} {a₁ : Solution₁ d} (h : IsFundamental a₁) {a : Solution₁ d} (hax : LT.lt 1 a.x) (hay : LT.lt 0 a.y) : LE.le a₁.y a.y

The y-coordinate of a fundamental solution is a lower bound for the y-coordinate of any positive solution.

theorem Pell.IsFundamental.x_mul_y_le_y_mul_x {d : Int} {a₁ : Solution₁ d} (h : IsFundamental a₁) {a : Solution₁ d} (hax : LT.lt 1 a.x) (hay : LT.lt 0 a.y) : LE.le (HMul.hMul a.x a₁.y) (HMul.hMul a.y a₁.x)

theorem Pell.IsFundamental.mul_inv_y_nonneg {d : Int} {a₁ : Solution₁ d} (h : IsFundamental a₁) {a : Solution₁ d} (hax : LT.lt 1 a.x) (hay : LT.lt 0 a.y) : LE.le 0 (HMul.hMul a (Inv.inv a₁)).y

If we multiply a positive solution with the inverse of a fundamental solution, the y-coordinate remains nonnegative.

theorem Pell.IsFundamental.mul_inv_x_pos {d : Int} {a₁ : Solution₁ d} (h : IsFundamental a₁) {a : Solution₁ d} (hax : LT.lt 1 a.x) (hay : LT.lt 0 a.y) : LT.lt 0 (HMul.hMul a (Inv.inv a₁)).x

If we multiply a positive solution with the inverse of a fundamental solution, the x-coordinate stays positive.

theorem Pell.IsFundamental.mul_inv_x_lt_x {d : Int} {a₁ : Solution₁ d} (h : IsFundamental a₁) {a : Solution₁ d} (hax : LT.lt 1 a.x) (hay : LT.lt 0 a.y) : LT.lt (HMul.hMul a (Inv.inv a₁)).x a.x

If we multiply a positive solution with the inverse of a fundamental solution, the x-coordinate decreases.

theorem Pell.IsFundamental.eq_pow_of_nonneg {d : Int} {a₁ : Solution₁ d} (h : IsFundamental a₁) {a : Solution₁ d} (hax : LT.lt 0 a.x) (hay : LE.le 0 a.y) : Exists fun (n : Nat) => Eq a (HPow.hPow a₁ n)

Any nonnegative solution is a power with nonnegative exponent of a fundamental solution.

theorem Pell.IsFundamental.eq_zpow_or_neg_zpow {d : Int} {a₁ : Solution₁ d} (h : IsFundamental a₁) (a : Solution₁ d) : Exists fun (n : Int) => Or (Eq a (HPow.hPow a₁ n)) (Eq a (Neg.neg (HPow.hPow a₁ n)))

Every solution is, up to a sign, a power of a given fundamental solution.

theorem Pell.existsUnique_pos_generator {d : Int} (h₀ : LT.lt 0 d) (hd : Not (IsSquare d)) : ExistsUnique fun (a₁ : Solution₁ d) => And (LT.lt 1 a₁.x) (And (LT.lt 0 a₁.y) (∀ (a : Solution₁ d), Exists fun (n : Int) => Or (Eq a (HPow.hPow a₁ n)) (Eq a (Neg.neg (HPow.hPow a₁ n)))))

When d is positive and not a square, then the group of solutions to the Pell equation x^2 - d*y^2 = 1 has a unique positive generator (up to sign).

theorem Pell.pos_generator_iff_fundamental {d : Int} (a : Solution₁ d) : Iff (And (LT.lt 1 a.x) (And (LT.lt 0 a.y) (∀ (b : Solution₁ d), Exists fun (n : Int) => Or (Eq b (HPow.hPow a n)) (Eq b (Neg.neg (HPow.hPow a n)))))) (IsFundamental a)

A positive solution is a generator (up to sign) of the group of all solutions to the Pell equation x^2 - d*y^2 = 1 if and only if it is a fundamental solution.