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)][IrelandRosen1990]
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.
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.
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
- Pell.Solution₁ d = ↥(unitary (ℤ√d))
Instances For
Equations
- Pell.Solution₁.instCommGroup = inferInstanceAs (CommGroup ↥(unitary (ℤ√d)))
Equations
- Pell.Solution₁.instHasDistribNeg = inferInstanceAs (HasDistribNeg ↥(unitary (ℤ√d)))
Equations
- Pell.Solution₁.instInhabited = inferInstanceAs (Inhabited ↥(unitary (ℤ√d)))
Equations
- Pell.Solution₁.instCoeSolution₁Zsqrtd = { coe := Subtype.val }
The x component of a solution to the Pell equation x^2 - d*y^2 = 1
Equations
- Pell.Solution₁.x a = (↑a).re
Instances For
The y component of a solution to the Pell equation x^2 - d*y^2 = 1
Equations
- Pell.Solution₁.y a = (↑a).im
Instances For
The proof that a is a solution to the Pell equation x^2 - d*y^2 = 1
An alternative form of the equation, suitable for rewriting x^2.
An alternative form of the equation, suitable for rewriting d * y^2.
Two solutions are equal if their x and y components are equal.
Construct a solution from x, y and a proof that the equation is satisfied.
Equations
- Pell.Solution₁.mk x y prop = { val := { re := x, im := y }, property := ⋯ }
Instances For
A solution has x ≠ 0.
If a solution has x > 1, then d is positive.
If a solution has x > 1, then d is not a square.
A solution with x = 1 is trivial.
A solution is 1 or -1 if and only if y = 0.
The set of solutions with x > 0 is closed under multiplication.
The set of solutions with x and y positive is closed under multiplication.
If (x, y) is a solution with x positive, then all its powers with natural exponents
have positive x.
If (x, y) is a solution with x and y positive, then all its powers with positive
natural exponents have positive y.
If (x, y) is a solution with x and y positive, then all its powers with positive
exponents have positive y.
If (x, y) is a solution with x positive, then all its powers have positive x.
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.
If a is any solution, then one of a, a⁻¹, -a, -a⁻¹ has
positive x and nonnegative y.
Existence of nontrivial solutions #
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.
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.
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
- Pell.IsFundamental a = (1 < Pell.Solution₁.x a ∧ 0 < Pell.Solution₁.y a ∧ ∀ {b : Pell.Solution₁ d}, 1 < Pell.Solution₁.x b → Pell.Solution₁.x a ≤ Pell.Solution₁.x b)
Instances For
A fundamental solution has positive x.
If a fundamental solution exists, then d must be positive.
If a fundamental solution exists, then d must be a non-square.
If there is a fundamental solution, it is unique.
If d is positive and not a square, then a fundamental solution exists.
The map sending an integer n to the y-coordinate of a^n for a fundamental
solution a is stritcly increasing.
If a is a fundamental solution, then (a^m).y < (a^n).y if and only if m < n.
The nth power of a fundamental solution is trivial if and only if n = 0.
A power of a fundamental solution is never equal to the negative of a power of this fundamental solution.
The x-coordinate of a fundamental solution is a lower bound for the x-coordinate
of any positive solution.
The y-coordinate of a fundamental solution is a lower bound for the y-coordinate
of any positive solution.
If we multiply a positive solution with the inverse of a fundamental solution,
the y-coordinate remains nonnegative.
If we multiply a positive solution with the inverse of a fundamental solution,
the x-coordinate stays positive.
If we multiply a positive solution with the inverse of a fundamental solution,
the x-coordinate decreases.
Any nonnegative solution is a power with nonnegative exponent of a fundamental solution.
Every solution is, up to a sign, a power of a given fundamental solution.
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).
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.