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 #
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₁.instCoeZsqrtd = { coe := Subtype.val }
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 = ⟨{ re := x, im := y }, ⋯⟩
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
positive, then all its powers have positive x
.
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
.
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.
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 n
th 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.