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

• pell is a function assigning to a natural number n the n-th solution to Pell's equation constructed recursively from the initial solution (0, 1).

Main statements

• eq_pell shows that every solution to Pell's equation is recursively obtained using pell
• matiyasevic shows that a certain system of Diophantine equations has a solution if and only if the first variable is the x-component in a solution to Pell's equation - the key step towards Hilbert's tenth problem in Davis' version of Matiyasevic's theorem.
• eq_pow_of_pell shows that the power function is Diophantine.

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

• [M. Carneiro, A Lean formalization of Matiyasevič's theorem][carneiro2018matiyasevic]
• [M. Davis, Hilbert's tenth problem is unsolvable][MR317916]

Tags

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

def Pell.IsPell {d : ℤ} : ℤ√d → Prop

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

theorem Pell.isPell_norm {d : ℤ} {b : ℤ√d} : IsPell b ↔ b * star b = 1

theorem Pell.isPell_iff_mem_unitary {d : ℤ} {b : ℤ√d} : IsPell b ↔ b ∈ unitary (ℤ√d)

theorem Pell.isPell_mul {d : ℤ} {b c : ℤ√d} (hb : IsPell b) (hc : IsPell c) : IsPell (b * c)

theorem Pell.isPell_star {d : ℤ} {b : ℤ√d} : IsPell b ↔ IsPell (star b)

@[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.

def Pell.xn {a : ℕ} (a1 : 1 < a) (n : ℕ) : ℕ

The Pell x sequence.

def Pell.yn {a : ℕ} (a1 : 1 < a) (n : ℕ) : ℕ

The Pell y sequence.

@[simp]

theorem Pell.pell_val {a : ℕ} (a1 : 1 < a) (n : ℕ) : pell a1 n = (xn a1 n, yn a1 n)

@[simp]

theorem Pell.xn_zero {a : ℕ} (a1 : 1 < a) : xn a1 0 = 1

@[simp]

theorem Pell.yn_zero {a : ℕ} (a1 : 1 < a) : yn a1 0 = 0

@[simp]

theorem Pell.xn_succ {a : ℕ} (a1 : 1 < a) (n : ℕ) : xn a1 (n + 1) = xn a1 n * a + Pell.d✝ a1 * yn a1 n

@[simp]

theorem Pell.yn_succ {a : ℕ} (a1 : 1 < a) (n : ℕ) : yn a1 (n + 1) = xn a1 n + yn a1 n * a

theorem Pell.xn_one {a : ℕ} (a1 : 1 < a) : xn a1 1 = a

theorem Pell.yn_one {a : ℕ} (a1 : 1 < a) : yn a1 1 = 1

def Pell.xz {a : ℕ} (a1 : 1 < a) (n : ℕ) : ℤ

The Pell x sequence, considered as an integer sequence.

def Pell.yz {a : ℕ} (a1 : 1 < a) (n : ℕ) : ℤ

The Pell y sequence, considered as an integer sequence.

def Pell.az (a : ℕ) : ℤ

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

theorem Pell.asq_pos {a : ℕ} (a1 : 1 < a) : 0 < a * a

theorem Pell.dz_val {a : ℕ} (a1 : 1 < a) : ↑(Pell.d✝ a1) = az a * az a - 1

@[simp]

theorem Pell.xz_succ {a : ℕ} (a1 : 1 < a) (n : ℕ) : xz a1 (n + 1) = xz a1 n * az a + ↑(Pell.d✝ a1) * yz a1 n

@[simp]

theorem Pell.yz_succ {a : ℕ} (a1 : 1 < a) (n : ℕ) : yz a1 (n + 1) = xz a1 n + yz a1 n * 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

@[simp]

theorem Pell.pellZd_re {a : ℕ} (a1 : 1 < a) (n : ℕ) : (pellZd a1 n).re = ↑(xn a1 n)

@[simp]

theorem Pell.pellZd_im {a : ℕ} (a1 : 1 < a) (n : ℕ) : (pellZd a1 n).im = ↑(yn a1 n)

theorem Pell.isPell_nat {a : ℕ} (a1 : 1 < a) {x y : ℕ} : IsPell { re := ↑x, im := ↑y } ↔ x * x - Pell.d✝ a1 * y * y = 1

@[simp]

theorem Pell.pellZd_succ {a : ℕ} (a1 : 1 < a) (n : ℕ) : pellZd a1 (n + 1) = pellZd a1 n * { re := ↑a, im := 1 }

theorem Pell.isPell_one {a : ℕ} (a1 : 1 < a) : IsPell { re := ↑a, im := 1 }

theorem Pell.isPell_pellZd {a : ℕ} (a1 : 1 < a) (n : ℕ) : IsPell (pellZd a1 n)

@[simp]

theorem Pell.pell_eqz {a : ℕ} (a1 : 1 < a) (n : ℕ) : xz a1 n * xz a1 n - ↑(Pell.d✝ a1) * yz a1 n * yz a1 n = 1

@[simp]

theorem Pell.pell_eq {a : ℕ} (a1 : 1 < a) (n : ℕ) : xn a1 n * xn a1 n - Pell.d✝ a1 * yn a1 n * yn a1 n = 1

instance Pell.dnsq {a : ℕ} (a1 : 1 < a) : Zsqrtd.Nonsquare (Pell.d✝ a1)

theorem Pell.xn_ge_a_pow {a : ℕ} (a1 : 1 < a) (n : ℕ) : a ^ n ≤ xn a1 n

theorem Pell.n_lt_xn {a : ℕ} (a1 : 1 < a) (n : ℕ) : n < xn a1 n

theorem Pell.x_pos {a : ℕ} (a1 : 1 < a) (n : ℕ) : 0 < xn a1 n

theorem Pell.eq_pell_lem {a : ℕ} (a1 : 1 < a) (n : ℕ) (b : ℤ√↑(Pell.d✝ a1)) : 1 ≤ b → IsPell b → b ≤ pellZd a1 n → ∃ (n : ℕ), b = pellZd a1 n

theorem Pell.eq_pellZd {a : ℕ} (a1 : 1 < a) (b : ℤ√↑(Pell.d✝ a1)) (b1 : 1 ≤ b) (hp : IsPell b) : ∃ (n : ℕ), b = pellZd a1 n

theorem Pell.eq_pell {a : ℕ} (a1 : 1 < a) {x y : ℕ} (hp : x * x - Pell.d✝ a1 * y * y = 1) : ∃ (n : ℕ), x = xn a1 n ∧ y = 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 : ℕ) : pellZd a1 (m + n) = pellZd a1 m * pellZd a1 n

theorem Pell.xn_add {a : ℕ} (a1 : 1 < a) (m n : ℕ) : xn a1 (m + n) = xn a1 m * xn a1 n + Pell.d✝ a1 * yn a1 m * yn a1 n

theorem Pell.yn_add {a : ℕ} (a1 : 1 < a) (m n : ℕ) : yn a1 (m + n) = xn a1 m * yn a1 n + yn a1 m * xn a1 n

theorem Pell.pellZd_sub {a : ℕ} (a1 : 1 < a) {m n : ℕ} (h : n ≤ m) : pellZd a1 (m - n) = pellZd a1 m * star (pellZd a1 n)

theorem Pell.xz_sub {a : ℕ} (a1 : 1 < a) {m n : ℕ} (h : n ≤ m) : xz a1 (m - n) = xz a1 m * xz a1 n - ↑(Pell.d✝ a1) * yz a1 m * yz a1 n

theorem Pell.yz_sub {a : ℕ} (a1 : 1 < a) {m n : ℕ} (h : n ≤ m) : yz a1 (m - n) = xz a1 n * yz a1 m - xz a1 m * yz a1 n

theorem Pell.xy_coprime {a : ℕ} (a1 : 1 < a) (n : ℕ) : (xn a1 n).Coprime (yn a1 n)

theorem Pell.strictMono_y {a : ℕ} (a1 : 1 < a) : StrictMono (yn a1)

theorem Pell.strictMono_x {a : ℕ} (a1 : 1 < a) : StrictMono (xn a1)

theorem Pell.yn_ge_n {a : ℕ} (a1 : 1 < a) (n : ℕ) : n ≤ yn a1 n

theorem Pell.y_mul_dvd {a : ℕ} (a1 : 1 < a) (n k : ℕ) : yn a1 n ∣ yn a1 (n * k)

theorem Pell.y_dvd_iff {a : ℕ} (a1 : 1 < a) (m n : ℕ) : yn a1 m ∣ yn a1 n ↔ m ∣ n

theorem Pell.xy_modEq_yn {a : ℕ} (a1 : 1 < a) (n k : ℕ) : xn a1 (n * k) ≡ xn a1 n ^ k [MOD yn a1 n ^ 2] ∧ yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD yn a1 n ^ 3]

theorem Pell.ysq_dvd_yy {a : ℕ} (a1 : 1 < a) (n : ℕ) : yn a1 n * yn a1 n ∣ yn a1 (n * yn a1 n)

theorem Pell.dvd_of_ysq_dvd {a : ℕ} (a1 : 1 < a) {n t : ℕ} (h : yn a1 n * yn a1 n ∣ yn a1 t) : yn a1 n ∣ t

theorem Pell.pellZd_succ_succ {a : ℕ} (a1 : 1 < a) (n : ℕ) : pellZd a1 (n + 2) + pellZd a1 n = ↑(2 * a) * pellZd a1 (n + 1)

theorem Pell.xy_succ_succ {a : ℕ} (a1 : 1 < a) (n : ℕ) : xn a1 (n + 2) + xn a1 n = 2 * a * xn a1 (n + 1) ∧ yn a1 (n + 2) + yn a1 n = 2 * a * yn a1 (n + 1)

theorem Pell.xn_succ_succ {a : ℕ} (a1 : 1 < a) (n : ℕ) : xn a1 (n + 2) + xn a1 n = 2 * a * xn a1 (n + 1)

theorem Pell.yn_succ_succ {a : ℕ} (a1 : 1 < a) (n : ℕ) : yn a1 (n + 2) + yn a1 n = 2 * a * yn a1 (n + 1)

theorem Pell.xz_succ_succ {a : ℕ} (a1 : 1 < a) (n : ℕ) : xz a1 (n + 2) = ↑(2 * a) * xz a1 (n + 1) - xz a1 n

theorem Pell.yz_succ_succ {a : ℕ} (a1 : 1 < a) (n : ℕ) : yz a1 (n + 2) = ↑(2 * a) * yz a1 (n + 1) - yz a1 n

theorem Pell.yn_modEq_a_sub_one {a : ℕ} (a1 : 1 < a) (n : ℕ) : yn a1 n ≡ n [MOD a - 1]

theorem Pell.yn_modEq_two {a : ℕ} (a1 : 1 < a) (n : ℕ) : 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 ∣ yz a1 n * (↑a - ↑y) + ↑(y ^ n) - xz a1 n

theorem Pell.xn_modEq_x2n_add_lem {a : ℕ} (a1 : 1 < a) (n j : ℕ) : xn a1 n ∣ Pell.d✝ a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j

theorem Pell.xn_modEq_x2n_add {a : ℕ} (a1 : 1 < a) (n j : ℕ) : xn a1 (2 * n + j) + xn a1 j ≡ 0 [MOD xn a1 n]

theorem Pell.xn_modEq_x2n_sub_lem {a : ℕ} (a1 : 1 < a) {n j : ℕ} (h : j ≤ n) : xn a1 (2 * n - j) + xn a1 j ≡ 0 [MOD xn a1 n]

theorem Pell.xn_modEq_x2n_sub {a : ℕ} (a1 : 1 < a) {n j : ℕ} (h : j ≤ 2 * n) : xn a1 (2 * n - j) + xn a1 j ≡ 0 [MOD xn a1 n]

theorem Pell.xn_modEq_x4n_add {a : ℕ} (a1 : 1 < a) (n j : ℕ) : xn a1 (4 * n + j) ≡ xn a1 j [MOD xn a1 n]

theorem Pell.xn_modEq_x4n_sub {a : ℕ} (a1 : 1 < a) {n j : ℕ} (h : j ≤ 2 * n) : xn a1 (4 * n - j) ≡ xn a1 j [MOD xn a1 n]

theorem Pell.eq_of_xn_modEq_lem1 {a : ℕ} (a1 : 1 < a) {i n j : ℕ} : i < j → j < n → xn a1 i % xn a1 n < xn a1 j % xn a1 n

theorem Pell.eq_of_xn_modEq_lem2 {a : ℕ} (a1 : 1 < a) {n : ℕ} (h : 2 * xn a1 n = 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 < j → j ≤ 2 * n → j ≠ n → ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j = 2) → xn a1 i % xn a1 n < xn a1 j % 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 : xn a1 i ≡ xn a1 j [MOD 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 : xn a1 i ≡ xn a1 j [MOD xn a1 n]) (ntriv : a = 2 → n = 1 → (i = 0 → j ≠ 2) ∧ (i = 2 → j ≠ 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 : xn a1 j ≡ xn a1 i [MOD 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 : xn a1 j ≡ xn a1 i [MOD 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 : ℕ) : xn a1 n ≡ xn b1 n [MOD c] ∧ yn a1 n ≡ yn b1 n [MOD c]

theorem Pell.matiyasevic {a k x y : ℕ} : (∃ (a1 : 1 < a), xn a1 k = x ∧ 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), xn a1 k ≡ 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)