Documentation

Mathlib.NumberTheory.PellMatiyasevic

Pell's equation and Matiyasevic's theorem #

This file solves Pell's equation, i.e. integer solutions to x ^ 2 - d * y ^ 2 = 1 in the special case that d = a ^ 2 - 1. This is then applied to prove Matiyasevic's theorem that the power function is Diophantine, which is the last key ingredient in the solution to Hilbert's tenth problem. For the definition of Diophantine function, see NumberTheory.Dioph.

For results on Pell's equation for arbitrary (positive, non-square) d, see NumberTheory.Pell.

Main definition #

Main statements #

Implementation notes #

The proof of Matiyasevic's theorem doesn't follow Matiyasevic's original account of using Fibonacci numbers but instead Davis' variant of using solutions to Pell's equation.

References #

Tags #

Pell's equation, Matiyasevic's theorem, Hilbert's tenth problem

def Pell.IsPell {d : } :

The property of being a solution to the Pell equation, expressed as a property of elements of ℤ√d.

Equations
Instances For
    theorem Pell.isPell_norm {d : } {b : ℤ√d} :
    theorem Pell.isPell_mul {d : } {b : ℤ√d} {c : ℤ√d} (hb : Pell.IsPell b) (hc : Pell.IsPell c) :
    @[simp]
    theorem Pell.d_pos {a : } (a1 : 1 < a) :
    0 < Pell.d a1
    def Pell.pell {a : } (a1 : 1 < a) :

    The Pell sequences, i.e. the sequence of integer solutions to x ^ 2 - d * y ^ 2 = 1, where d = a ^ 2 - 1, defined together in mutual recursion.

    Equations
    Instances For
      def Pell.xn {a : } (a1 : 1 < a) (n : ) :

      The Pell x sequence.

      Equations
      Instances For
        def Pell.yn {a : } (a1 : 1 < a) (n : ) :

        The Pell y sequence.

        Equations
        Instances For
          @[simp]
          theorem Pell.pell_val {a : } (a1 : 1 < a) (n : ) :
          Pell.pell a1 n = (Pell.xn a1 n, Pell.yn a1 n)
          @[simp]
          theorem Pell.xn_zero {a : } (a1 : 1 < a) :
          Pell.xn a1 0 = 1
          @[simp]
          theorem Pell.yn_zero {a : } (a1 : 1 < a) :
          Pell.yn a1 0 = 0
          @[simp]
          theorem Pell.xn_succ {a : } (a1 : 1 < a) (n : ) :
          Pell.xn a1 (n + 1) = Pell.xn a1 n * a + Pell.d a1 * Pell.yn a1 n
          @[simp]
          theorem Pell.yn_succ {a : } (a1 : 1 < a) (n : ) :
          Pell.yn a1 (n + 1) = Pell.xn a1 n + Pell.yn a1 n * a
          theorem Pell.xn_one {a : } (a1 : 1 < a) :
          Pell.xn a1 1 = a
          theorem Pell.yn_one {a : } (a1 : 1 < a) :
          Pell.yn a1 1 = 1
          def Pell.xz {a : } (a1 : 1 < a) (n : ) :

          The Pell x sequence, considered as an integer sequence.

          Equations
          Instances For
            def Pell.yz {a : } (a1 : 1 < a) (n : ) :

            The Pell y sequence, considered as an integer sequence.

            Equations
            Instances For
              def Pell.az (a : ) :

              The element a such that d = a ^ 2 - 1, considered as an integer.

              Equations
              Instances For
                theorem Pell.asq_pos {a : } (a1 : 1 < a) :
                0 < a * a
                theorem Pell.dz_val {a : } (a1 : 1 < a) :
                (Pell.d a1) = Pell.az a * Pell.az a - 1
                @[simp]
                theorem Pell.xz_succ {a : } (a1 : 1 < a) (n : ) :
                Pell.xz a1 (n + 1) = Pell.xz a1 n * Pell.az a + (Pell.d a1) * Pell.yz a1 n
                @[simp]
                theorem Pell.yz_succ {a : } (a1 : 1 < a) (n : ) :
                Pell.yz a1 (n + 1) = Pell.xz a1 n + Pell.yz a1 n * Pell.az a
                def Pell.pellZd {a : } (a1 : 1 < a) (n : ) :
                ℤ√(Pell.d a1)

                The Pell sequence can also be viewed as an element of ℤ√d

                Equations
                Instances For
                  @[simp]
                  theorem Pell.pellZd_re {a : } (a1 : 1 < a) (n : ) :
                  (Pell.pellZd a1 n).re = (Pell.xn a1 n)
                  @[simp]
                  theorem Pell.pellZd_im {a : } (a1 : 1 < a) (n : ) :
                  (Pell.pellZd a1 n).im = (Pell.yn a1 n)
                  theorem Pell.isPell_nat {a : } (a1 : 1 < a) {x : } {y : } :
                  Pell.IsPell { re := x, im := y } x * x - Pell.d a1 * y * y = 1
                  @[simp]
                  theorem Pell.pellZd_succ {a : } (a1 : 1 < a) (n : ) :
                  Pell.pellZd a1 (n + 1) = Pell.pellZd a1 n * { re := a, im := 1 }
                  theorem Pell.isPell_one {a : } (a1 : 1 < a) :
                  Pell.IsPell { re := a, im := 1 }
                  theorem Pell.isPell_pellZd {a : } (a1 : 1 < a) (n : ) :
                  @[simp]
                  theorem Pell.pell_eqz {a : } (a1 : 1 < a) (n : ) :
                  Pell.xz a1 n * Pell.xz a1 n - (Pell.d a1) * Pell.yz a1 n * Pell.yz a1 n = 1
                  @[simp]
                  theorem Pell.pell_eq {a : } (a1 : 1 < a) (n : ) :
                  Pell.xn a1 n * Pell.xn a1 n - Pell.d a1 * Pell.yn a1 n * Pell.yn a1 n = 1
                  instance Pell.dnsq {a : } (a1 : 1 < a) :
                  Equations
                  • =
                  theorem Pell.xn_ge_a_pow {a : } (a1 : 1 < a) (n : ) :
                  a ^ n Pell.xn a1 n
                  theorem Pell.n_lt_a_pow {a : } (a1 : 1 < a) (n : ) :
                  n < a ^ n
                  theorem Pell.n_lt_xn {a : } (a1 : 1 < a) (n : ) :
                  n < Pell.xn a1 n
                  theorem Pell.x_pos {a : } (a1 : 1 < a) (n : ) :
                  0 < Pell.xn a1 n
                  theorem Pell.eq_pell_lem {a : } (a1 : 1 < a) (n : ) (b : ℤ√(Pell.d a1)) :
                  1 bPell.IsPell bb Pell.pellZd a1 n∃ (n : ), b = Pell.pellZd a1 n
                  theorem Pell.eq_pellZd {a : } (a1 : 1 < a) (b : ℤ√(Pell.d a1)) (b1 : 1 b) (hp : Pell.IsPell b) :
                  ∃ (n : ), b = Pell.pellZd a1 n
                  theorem Pell.eq_pell {a : } (a1 : 1 < a) {x : } {y : } (hp : x * x - Pell.d a1 * y * y = 1) :
                  ∃ (n : ), x = Pell.xn a1 n y = Pell.yn a1 n

                  Every solution to Pell's equation is recursively obtained from the initial solution (1,0) using the recursion pell.

                  theorem Pell.pellZd_add {a : } (a1 : 1 < a) (m : ) (n : ) :
                  Pell.pellZd a1 (m + n) = Pell.pellZd a1 m * Pell.pellZd a1 n
                  theorem Pell.xn_add {a : } (a1 : 1 < a) (m : ) (n : ) :
                  Pell.xn a1 (m + n) = Pell.xn a1 m * Pell.xn a1 n + Pell.d a1 * Pell.yn a1 m * Pell.yn a1 n
                  theorem Pell.yn_add {a : } (a1 : 1 < a) (m : ) (n : ) :
                  Pell.yn a1 (m + n) = Pell.xn a1 m * Pell.yn a1 n + Pell.yn a1 m * Pell.xn a1 n
                  theorem Pell.pellZd_sub {a : } (a1 : 1 < a) {m : } {n : } (h : n m) :
                  Pell.pellZd a1 (m - n) = Pell.pellZd a1 m * star (Pell.pellZd a1 n)
                  theorem Pell.xz_sub {a : } (a1 : 1 < a) {m : } {n : } (h : n m) :
                  Pell.xz a1 (m - n) = Pell.xz a1 m * Pell.xz a1 n - (Pell.d a1) * Pell.yz a1 m * Pell.yz a1 n
                  theorem Pell.yz_sub {a : } (a1 : 1 < a) {m : } {n : } (h : n m) :
                  Pell.yz a1 (m - n) = Pell.xz a1 n * Pell.yz a1 m - Pell.xz a1 m * Pell.yz a1 n
                  theorem Pell.xy_coprime {a : } (a1 : 1 < a) (n : ) :
                  (Pell.xn a1 n).Coprime (Pell.yn a1 n)
                  theorem Pell.strictMono_y {a : } (a1 : 1 < a) :
                  theorem Pell.strictMono_x {a : } (a1 : 1 < a) :
                  theorem Pell.yn_ge_n {a : } (a1 : 1 < a) (n : ) :
                  n Pell.yn a1 n
                  theorem Pell.y_mul_dvd {a : } (a1 : 1 < a) (n : ) (k : ) :
                  Pell.yn a1 n Pell.yn a1 (n * k)
                  theorem Pell.y_dvd_iff {a : } (a1 : 1 < a) (m : ) (n : ) :
                  Pell.yn a1 m Pell.yn a1 n m n
                  theorem Pell.xy_modEq_yn {a : } (a1 : 1 < a) (n : ) (k : ) :
                  Pell.xn a1 (n * k) Pell.xn a1 n ^ k [MOD Pell.yn a1 n ^ 2] Pell.yn a1 (n * k) k * Pell.xn a1 n ^ (k - 1) * Pell.yn a1 n [MOD Pell.yn a1 n ^ 3]
                  theorem Pell.ysq_dvd_yy {a : } (a1 : 1 < a) (n : ) :
                  Pell.yn a1 n * Pell.yn a1 n Pell.yn a1 (n * Pell.yn a1 n)
                  theorem Pell.dvd_of_ysq_dvd {a : } (a1 : 1 < a) {n : } {t : } (h : Pell.yn a1 n * Pell.yn a1 n Pell.yn a1 t) :
                  Pell.yn a1 n t
                  theorem Pell.pellZd_succ_succ {a : } (a1 : 1 < a) (n : ) :
                  Pell.pellZd a1 (n + 2) + Pell.pellZd a1 n = (2 * a) * Pell.pellZd a1 (n + 1)
                  theorem Pell.xy_succ_succ {a : } (a1 : 1 < a) (n : ) :
                  Pell.xn a1 (n + 2) + Pell.xn a1 n = 2 * a * Pell.xn a1 (n + 1) Pell.yn a1 (n + 2) + Pell.yn a1 n = 2 * a * Pell.yn a1 (n + 1)
                  theorem Pell.xn_succ_succ {a : } (a1 : 1 < a) (n : ) :
                  Pell.xn a1 (n + 2) + Pell.xn a1 n = 2 * a * Pell.xn a1 (n + 1)
                  theorem Pell.yn_succ_succ {a : } (a1 : 1 < a) (n : ) :
                  Pell.yn a1 (n + 2) + Pell.yn a1 n = 2 * a * Pell.yn a1 (n + 1)
                  theorem Pell.xz_succ_succ {a : } (a1 : 1 < a) (n : ) :
                  Pell.xz a1 (n + 2) = (2 * a) * Pell.xz a1 (n + 1) - Pell.xz a1 n
                  theorem Pell.yz_succ_succ {a : } (a1 : 1 < a) (n : ) :
                  Pell.yz a1 (n + 2) = (2 * a) * Pell.yz a1 (n + 1) - Pell.yz a1 n
                  theorem Pell.yn_modEq_a_sub_one {a : } (a1 : 1 < a) (n : ) :
                  Pell.yn a1 n n [MOD a - 1]
                  theorem Pell.yn_modEq_two {a : } (a1 : 1 < a) (n : ) :
                  Pell.yn a1 n n [MOD 2]
                  theorem Pell.x_sub_y_dvd_pow_lem (y2 : ) (y1 : ) (y0 : ) (yn1 : ) (yn0 : ) (xn1 : ) (xn0 : ) (ay : ) (a2 : ) :
                  (a2 * yn1 - yn0) * ay + y2 - (a2 * xn1 - xn0) = y2 - a2 * y1 + y0 + a2 * (yn1 * ay + y1 - xn1) - (yn0 * ay + y0 - xn0)
                  theorem Pell.x_sub_y_dvd_pow {a : } (a1 : 1 < a) (y : ) (n : ) :
                  2 * a * y - y * y - 1 Pell.yz a1 n * (a - y) + (y ^ n) - Pell.xz a1 n
                  theorem Pell.xn_modEq_x2n_add_lem {a : } (a1 : 1 < a) (n : ) (j : ) :
                  Pell.xn a1 n Pell.d a1 * Pell.yn a1 n * (Pell.yn a1 n * Pell.xn a1 j) + Pell.xn a1 j
                  theorem Pell.xn_modEq_x2n_add {a : } (a1 : 1 < a) (n : ) (j : ) :
                  Pell.xn a1 (2 * n + j) + Pell.xn a1 j 0 [MOD Pell.xn a1 n]
                  theorem Pell.xn_modEq_x2n_sub_lem {a : } (a1 : 1 < a) {n : } {j : } (h : j n) :
                  Pell.xn a1 (2 * n - j) + Pell.xn a1 j 0 [MOD Pell.xn a1 n]
                  theorem Pell.xn_modEq_x2n_sub {a : } (a1 : 1 < a) {n : } {j : } (h : j 2 * n) :
                  Pell.xn a1 (2 * n - j) + Pell.xn a1 j 0 [MOD Pell.xn a1 n]
                  theorem Pell.xn_modEq_x4n_add {a : } (a1 : 1 < a) (n : ) (j : ) :
                  Pell.xn a1 (4 * n + j) Pell.xn a1 j [MOD Pell.xn a1 n]
                  theorem Pell.xn_modEq_x4n_sub {a : } (a1 : 1 < a) {n : } {j : } (h : j 2 * n) :
                  Pell.xn a1 (4 * n - j) Pell.xn a1 j [MOD Pell.xn a1 n]
                  theorem Pell.eq_of_xn_modEq_lem1 {a : } (a1 : 1 < a) {i : } {n : } {j : } :
                  i < jj < nPell.xn a1 i % Pell.xn a1 n < Pell.xn a1 j % Pell.xn a1 n
                  theorem Pell.eq_of_xn_modEq_lem2 {a : } (a1 : 1 < a) {n : } (h : 2 * Pell.xn a1 n = Pell.xn a1 (n + 1)) :
                  a = 2 n = 0
                  theorem Pell.eq_of_xn_modEq_lem3 {a : } (a1 : 1 < a) {i : } {n : } (npos : 0 < n) {j : } :
                  i < jj 2 * nj n¬(a = 2 n = 1 i = 0 j = 2)Pell.xn a1 i % Pell.xn a1 n < Pell.xn a1 j % Pell.xn a1 n
                  theorem Pell.eq_of_xn_modEq_le {a : } (a1 : 1 < a) {i : } {j : } {n : } (ij : i j) (j2n : j 2 * n) (h : Pell.xn a1 i Pell.xn a1 j [MOD Pell.xn a1 n]) (ntriv : ¬(a = 2 n = 1 i = 0 j = 2)) :
                  i = j
                  theorem Pell.eq_of_xn_modEq {a : } (a1 : 1 < a) {i : } {j : } {n : } (i2n : i 2 * n) (j2n : j 2 * n) (h : Pell.xn a1 i Pell.xn a1 j [MOD Pell.xn a1 n]) (ntriv : a = 2n = 1(i = 0j 2) (i = 2j 0)) :
                  i = j
                  theorem Pell.eq_of_xn_modEq' {a : } (a1 : 1 < a) {i : } {j : } {n : } (ipos : 0 < i) (hin : i n) (j4n : j 4 * n) (h : Pell.xn a1 j Pell.xn a1 i [MOD Pell.xn a1 n]) :
                  j = i j + i = 4 * n
                  theorem Pell.modEq_of_xn_modEq {a : } (a1 : 1 < a) {i : } {j : } {n : } (ipos : 0 < i) (hin : i n) (h : Pell.xn a1 j Pell.xn a1 i [MOD Pell.xn a1 n]) :
                  j i [MOD 4 * n] j + i 0 [MOD 4 * n]
                  theorem Pell.xy_modEq_of_modEq {a : } {b : } {c : } (a1 : 1 < a) (b1 : 1 < b) (h : a b [MOD c]) (n : ) :
                  Pell.xn a1 n Pell.xn b1 n [MOD c] Pell.yn a1 n Pell.yn b1 n [MOD c]
                  theorem Pell.matiyasevic {a : } {k : } {x : } {y : } :
                  (∃ (a1 : 1 < a), Pell.xn a1 k = x Pell.yn a1 k = y) 1 < a k y (x = 1 y = 0 ∃ (u : ) (v : ) (s : ) (t : ) (b : ), x * x - (a * a - 1) * y * y = 1 u * u - (a * a - 1) * v * v = 1 s * s - (b * b - 1) * t * t = 1 1 < b b 1 [MOD 4 * y] b a [MOD u] 0 < v y * y v s x [MOD u] t k [MOD 4 * y])
                  theorem Pell.eq_pow_of_pell_lem {a : } {y : } {k : } (hy0 : y 0) (hk0 : k 0) (hyk : y ^ k < a) :
                  (y ^ k) < 2 * a * y - y * y - 1
                  theorem Pell.eq_pow_of_pell {m : } {n : } {k : } :
                  n ^ k = m k = 0 m = 1 0 < k (n = 0 m = 0 0 < n ∃ (w : ) (a : ) (t : ) (z : ) (a1 : 1 < a), Pell.xn a1 k Pell.yn a1 k * (a - n) + m [MOD t] 2 * a * n = t + (n * n + 1) m < t n w k w a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1)