mathlib3 documentation

number_theory.pell

Pell's Equation #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 number_theory.pell_matiyasevic, 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_is_square and pell.solution₁.exists_nontrivial_of_not_is_square.

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.is_fundamental.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 #

Tags #

Pell's equation

TODO #

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.

source
theorem pell.is_pell_solution_iff_mem_unitary {d : ℤ} {a : ℤ√d} :
a.re ^ 2 - d * a.im ^ 2 = 1 ↔ a ∈ unitary (ℤ√d)

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.is_pell_iff_mem_unitary.

source
def pell.solution₁ (d : ℤ) :
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
Instances for pell.solution₁
source
@[protected, instance]
def pell.solution₁.comm_group (d : ℤ) :
comm_group (pell.solution₁ d)
source
@[protected, instance]
def pell.solution₁.has_distrib_neg (d : ℤ) :
has_distrib_neg (pell.solution₁ d)
source
@[protected, instance]
def pell.solution₁.inhabited (d : ℤ) :
inhabited (pell.solution₁ d)
source
@[protected, instance]
def pell.solution₁.zsqrtd.has_coe {d : ℤ} :
has_coe (pell.solution₁ d) (ℤ√d)
Equations
source
@[protected]
def pell.solution₁.x {d : ℤ} (a : pell.solution₁ d) :
ℤ

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

Equations
source
@[protected]
def pell.solution₁.y {d : ℤ} (a : pell.solution₁ d) :
ℤ

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

Equations
source
theorem pell.solution₁.prop {d : ℤ} (a : pell.solution₁ d) :
a.x ^ 2 - d * a.y ^ 2 = 1

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

source
theorem pell.solution₁.prop_x {d : ℤ} (a : pell.solution₁ d) :
a.x ^ 2 = 1 + d * a.y ^ 2

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

source
theorem pell.solution₁.prop_y {d : ℤ} (a : pell.solution₁ d) :
d * a.y ^ 2 = a.x ^ 2 - 1

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

source
@[ext]
theorem pell.solution₁.ext {d : ℤ} {a b : pell.solution₁ d} (hx : a.x = b.x) (hy : a.y = b.y) :
a = b

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

source
def pell.solution₁.mk {d : ℤ} (x y : ℤ) (prop : x ^ 2 - d * y ^ 2 = 1) :
pell.solution₁ d

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

Equations
source
@[simp]
theorem pell.solution₁.x_mk {d : ℤ} (x y : ℤ) (prop : x ^ 2 - d * y ^ 2 = 1) :
(pell.solution₁.mk x y prop).x = x
source
@[simp]
theorem pell.solution₁.y_mk {d : ℤ} (x y : ℤ) (prop : x ^ 2 - d * y ^ 2 = 1) :
(pell.solution₁.mk x y prop).y = y
source
@[simp]
theorem pell.solution₁.coe_mk {d : ℤ} (x y : ℤ) (prop : x ^ 2 - d * y ^ 2 = 1) :
↑(pell.solution₁.mk x y prop) = {re := x, im := y}
source
@[simp]
theorem pell.solution₁.x_one {d : ℤ} :
1.x = 1
source
@[simp]
theorem pell.solution₁.y_one {d : ℤ} :
1.y = 0
source
@[simp]
theorem pell.solution₁.x_mul {d : ℤ} (a b : pell.solution₁ d) :
(a * b).x = a.x * b.x + d * (a.y * b.y)
source
@[simp]
theorem pell.solution₁.y_mul {d : ℤ} (a b : pell.solution₁ d) :
(a * b).y = a.x * b.y + a.y * b.x
source
@[simp]
theorem pell.solution₁.x_inv {d : ℤ} (a : pell.solution₁ d) :
a⁻¹.x = a.x
source
@[simp]
theorem pell.solution₁.y_inv {d : ℤ} (a : pell.solution₁ d) :
a⁻¹.y = -a.y
source
@[simp]
theorem pell.solution₁.x_neg {d : ℤ} (a : pell.solution₁ d) :
(-a).x = -a.x
source
@[simp]
theorem pell.solution₁.y_neg {d : ℤ} (a : pell.solution₁ d) :
(-a).y = -a.y
source
theorem pell.solution₁.eq_zero_of_d_neg {d : ℤ} (h₀ : d < 0) (a : pell.solution₁ d) :
a.x = 0 ∨ a.y = 0

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

source
theorem pell.solution₁.x_ne_zero {d : ℤ} (h₀ : 0 ≤ d) (a : pell.solution₁ d) :
a.x ≠ 0

A solution has x ≠ 0.

source
theorem pell.solution₁.y_ne_zero_of_one_lt_x {d : ℤ} {a : pell.solution₁ d} (ha : 1 < a.x) :
a.y ≠ 0

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

source
theorem pell.solution₁.d_pos_of_one_lt_x {d : ℤ} {a : pell.solution₁ d} (ha : 1 < a.x) :
0 < d

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

source
theorem pell.solution₁.d_nonsquare_of_one_lt_x {d : ℤ} {a : pell.solution₁ d} (ha : 1 < a.x) :
¬is_square d

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

source
theorem pell.solution₁.eq_one_of_x_eq_one {d : ℤ} (h₀ : d ≠ 0) {a : pell.solution₁ d} (ha : a.x = 1) :
a = 1

A solution with x = 1 is trivial.

source
theorem pell.solution₁.eq_one_or_neg_one_iff_y_eq_zero {d : ℤ} {a : pell.solution₁ d} :
a = 1 ∨ a = -1 ↔ a.y = 0

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

source
theorem pell.solution₁.x_mul_pos {d : ℤ} {a b : pell.solution₁ d} (ha : 0 < a.x) (hb : 0 < b.x) :
0 < (a * b).x

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

source
theorem pell.solution₁.y_mul_pos {d : ℤ} {a b : pell.solution₁ d} (hax : 0 < a.x) (hay : 0 < a.y) (hbx : 0 < b.x) (hby : 0 < b.y) :
0 < (a * b).y

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

source
theorem pell.solution₁.x_pow_pos {d : ℤ} {a : pell.solution₁ d} (hax : 0 < a.x) (n : ℕ) :
0 < (a ^ n).x

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

source
theorem pell.solution₁.y_pow_succ_pos {d : ℤ} {a : pell.solution₁ d} (hax : 0 < a.x) (hay : 0 < a.y) (n : ℕ) :
0 < (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.

source
theorem pell.solution₁.y_zpow_pos {d : ℤ} {a : pell.solution₁ d} (hax : 0 < a.x) (hay : 0 < a.y) {n : ℤ} (hn : 0 < n) :
0 < (a ^ n).y

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

source
theorem pell.solution₁.x_zpow_pos {d : ℤ} {a : pell.solution₁ d} (hax : 0 < a.x) (n : ℤ) :
0 < (a ^ n).x

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

source
theorem pell.solution₁.sign_y_zpow_eq_sign_of_x_pos_of_y_pos {d : ℤ} {a : pell.solution₁ d} (hax : 0 < a.x) (hay : 0 < a.y) (n : ℤ) :
(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.

source
theorem pell.solution₁.exists_pos_variant {d : ℤ} (h₀ : 0 < d) (a : pell.solution₁ d) :
∃ (b : pell.solution₁ d), 0 < b.x ∧ 0 ≤ b.y ∧ a ∈ {b, b⁻¹, -b, -b⁻¹}

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

Existence of nontrivial solutions #

source
theorem pell.exists_of_not_is_square {d : ℤ} (h₀ : 0 < d) (hd : ¬is_square d) :
∃ (x y : ℤ), x ^ 2 - d * y ^ 2 = 1 ∧ 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.

source
theorem pell.exists_iff_not_is_square {d : ℤ} (h₀ : 0 < d) :
(∃ (x y : ℤ), x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0) ↔ ¬is_square 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.

source
theorem pell.solution₁.exists_nontrivial_of_not_is_square {d : ℤ} (h₀ : 0 < d) (hd : ¬is_square d) :
∃ (a : pell.solution₁ d), a ≠ 1 ∧ 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.

source
theorem pell.solution₁.exists_pos_of_not_is_square {d : ℤ} (h₀ : 0 < d) (hd : ¬is_square d) :
∃ (a : pell.solution₁ d), 1 < a.x ∧ 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.

source
def pell.is_fundamental {d : ℤ} (a : pell.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
source
theorem pell.is_fundamental.x_pos {d : ℤ} {a : pell.solution₁ d} (h : pell.is_fundamental a) :
0 < a.x

A fundamental solution has positive x.

source
theorem pell.is_fundamental.d_pos {d : ℤ} {a : pell.solution₁ d} (h : pell.is_fundamental a) :
0 < d

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

source
theorem pell.is_fundamental.d_nonsquare {d : ℤ} {a : pell.solution₁ d} (h : pell.is_fundamental a) :
¬is_square d

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

source
theorem pell.is_fundamental.subsingleton {d : ℤ} {a b : pell.solution₁ d} (ha : pell.is_fundamental a) (hb : pell.is_fundamental b) :
a = b

If there is a fundamental solution, it is unique.

source
theorem pell.is_fundamental.exists_of_not_is_square {d : ℤ} (h₀ : 0 < d) (hd : ¬is_square d) :
∃ (a : pell.solution₁ d), pell.is_fundamental a

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

source
theorem pell.is_fundamental.y_strict_mono {d : ℤ} {a : pell.solution₁ d} (h : pell.is_fundamental a) :
strict_mono (λ (n : ℤ), (a ^ n).y)

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

source
theorem pell.is_fundamental.zpow_y_lt_iff_lt {d : ℤ} {a : pell.solution₁ d} (h : pell.is_fundamental a) (m n : ℤ) :
(a ^ m).y < (a ^ n).y ↔ m < n

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

source
theorem pell.is_fundamental.zpow_eq_one_iff {d : ℤ} {a : pell.solution₁ d} (h : pell.is_fundamental a) (n : ℤ) :
a ^ n = 1 ↔ n = 0

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

source
theorem pell.is_fundamental.zpow_ne_neg_zpow {d : ℤ} {a : pell.solution₁ d} (h : pell.is_fundamental a) {n n' : ℤ} :
a ^ n ≠ -a ^ n'

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

source
theorem pell.is_fundamental.x_le_x {d : ℤ} {a₁ : pell.solution₁ d} (h : pell.is_fundamental a₁) {a : pell.solution₁ d} (hax : 1 < a.x) :
a₁.x ≤ a.x

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

source
theorem pell.is_fundamental.y_le_y {d : ℤ} {a₁ : pell.solution₁ d} (h : pell.is_fundamental a₁) {a : pell.solution₁ d} (hax : 1 < a.x) (hay : 0 < a.y) :
a₁.y ≤ a.y

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

source
theorem pell.is_fundamental.x_mul_y_le_y_mul_x {d : ℤ} {a₁ : pell.solution₁ d} (h : pell.is_fundamental a₁) {a : pell.solution₁ d} (hax : 1 < a.x) (hay : 0 < a.y) :
a.x * a₁.y ≤ a.y * a₁.x
source
theorem pell.is_fundamental.mul_inv_y_nonneg {d : ℤ} {a₁ : pell.solution₁ d} (h : pell.is_fundamental a₁) {a : pell.solution₁ d} (hax : 1 < a.x) (hay : 0 < a.y) :
0 ≤ (a * a₁⁻¹).y

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

source
theorem pell.is_fundamental.mul_inv_x_pos {d : ℤ} {a₁ : pell.solution₁ d} (h : pell.is_fundamental a₁) {a : pell.solution₁ d} (hax : 1 < a.x) (hay : 0 < a.y) :
0 < (a * a₁⁻¹).x

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

source
theorem pell.is_fundamental.mul_inv_x_lt_x {d : ℤ} {a₁ : pell.solution₁ d} (h : pell.is_fundamental a₁) {a : pell.solution₁ d} (hax : 1 < a.x) (hay : 0 < a.y) :
(a * a₁⁻¹).x < a.x

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

source
theorem pell.is_fundamental.eq_pow_of_nonneg {d : ℤ} {a₁ : pell.solution₁ d} (h : pell.is_fundamental a₁) {a : pell.solution₁ d} (hax : 0 < a.x) (hay : 0 ≤ a.y) :
∃ (n : ℕ), a = a₁ ^ n

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

source
theorem pell.is_fundamental.eq_zpow_or_neg_zpow {d : ℤ} {a₁ : pell.solution₁ d} (h : pell.is_fundamental a₁) (a : pell.solution₁ d) :
∃ (n : ℤ), a = a₁ ^ n ∨ a = -a₁ ^ n

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

source
theorem pell.exists_unique_pos_generator {d : ℤ} (h₀ : 0 < d) (hd : ¬is_square d) :
∃! (a₁ : pell.solution₁ d), 1 < a₁.x ∧ 0 < a₁.y ∧ ∀ (a : pell.solution₁ d), ∃ (n : ℤ), a = a₁ ^ n ∨ a = -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).

source
theorem pell.pos_generator_iff_fundamental {d : ℤ} (a : pell.solution₁ d) :
(1 < a.x ∧ 0 < a.y ∧ ∀ (b : pell.solution₁ d), ∃ (n : ℤ), b = a ^ n ∨ b = -a ^ n) ↔ pell.is_fundamental 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.