Pell's equation

TheoremComposing a Pell-type solution with a norm-one unit#✓fully proved

Let \(a, b, c, T, U, x, y\) be integers with \(a T^2 - b U^2 = c\) and \(x^2 - ab y^2 = 1\). Then the pair \((T x + b U y, a T y + U x)\) is again a solution: \(a (T x + b U y)^2 - b (a T y + U x)^2 = c\).

The source iterates this step, assuming that \(ab > 1\) is not a square, to obtain infinitely many solutions. That conclusion needs further nondegeneracy hypotheses (for \(T = U = c = 0\) every iterate is \((0, 0)\)); the single step is the multiplicativity of the norm form and needs no hypotheses beyond the two equations.

theorem pellType_solution_mul_unit
    (a b c T U x y : ℤ)
    (hsol : a * T ^ 2 - b * U ^ 2 = c)
    (hunit : x ^ 2 - a * b * y ^ 2 = 1) :
    a * (T * x + b * U * y) ^ 2 - b * (a * T * y + U * x) ^ 2 = c
Sources

TheoremSolutions of Pell's equation are continued-fraction convergents#●ready to prove

Let \(d\) be a positive squarefree integer and let \(x\) and \(y\) be positive integers with \(x^2 - d y^2 = 1\). Then \(x / y\) is a convergent of the regular continued fraction expansion of \(\sqrt{d}\): there is a natural number \(n\) such that the \(n\)-th convergent of \(\sqrt{d}\) (counting from the \(0\)-th) equals \(x / y\).

public theorem_wanted pell_solution_is_convergent
    (d : ℤ) (_hd : Squarefree d) (_hd0 : 0 < d)
    (x y : ℤ) (_hx : 0 < x) (_hy : 0 < y)
    (_hsol : x ^ 2 - d * y ^ 2 = 1) :
    ∃ n : ℕ, (GenContFract.of (Real.sqrt (d : ℝ))).convs n = (x : ℝ) / (y : ℝ)
Sources
  • J.-L. Lagrange (1770). Listed as §84 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Problem pell_solution_convergent of the lean-eval benchmark.
1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.