English
There exists a Diophantine encoding of Pell-type equations linking sequences xn and yn to four-tuples of naturals with Pell-structure.
Русский
Существует диофантова кодировка уравнений типа Пелля, связывающая последовательности x_n и y_n с четырёхпараметрическими натуральными величинами в рамках Пелль-структуры.
LaTeX
$$$$\\mathrm{Dioph}\\;\\bigl(\\lambda v. \\exists h:\\mathbb{N},\\; \\mathrm{Pell.xn}\\;h(v_1)=v_2 \\wedge \\mathrm{Pell.yn}\\;h(v_1)=v_3\\bigr).$$$$
Lean4
theorem pell_dioph : Dioph fun v : Vector3 ℕ 4 => ∃ h : 1 < v &0, xn h (v &1) = v &2 ∧ yn h (v &1) = v &3 :=
by
have :
Dioph
{v : Vector3 ℕ 4 |
1 < v &0 ∧
v &1 ≤ v &3 ∧
(v &2 = 1 ∧ v &3 = 0 ∨
∃ u w s t b : ℕ,
v &2 * v &2 - (v &0 * v &0 - 1) * v &3 * v &3 = 1 ∧
u * u - (v &0 * v &0 - 1) * w * w = 1 ∧
s * s - (b * b - 1) * t * t = 1 ∧
1 < b ∧
b ≡ 1 [MOD 4 * v &3] ∧
b ≡ v &0 [MOD u] ∧ 0 < w ∧ v &3 * v &3 ∣ w ∧ s ≡ v &2 [MOD u] ∧ t ≡ v &1 [MOD 4 * v &3])} :=
(D.1 D< D&0 D∧
D&1 D≤ D&3 D∧
((D&2 D= D.1 D∧ D&3 D= D.0) D∨
((D∃) 4 <|
(D∃) 5 <|
(D∃) 6 <|
(D∃) 7 <|
(D∃) 8 <|
D&7 D* D&7 D- (D&5 D* D&5 D- D.1) D* D&8 D* D&8 D= D.1 D∧
D&4 D* D&4 D- (D&5 D* D&5 D- D.1) D* D&3 D* D&3 D= D.1 D∧
D&2 D* D&2 D- (D&0 D* D&0 D- D.1) D* D&1 D* D&1 D= D.1 D∧
D.1 D< D&0 D∧
( D≡ (D&0) (D.1) (D.4 D* D&8)) D∧
( D≡ (D&0) (D&5) (D&4)) D∧
D.0 D< D&3 D∧
D&8 D* D&8 D∣ D&3 D∧
( D≡ (D&2) (D&7) (D&4)) D∧ ( D≡ (D&1) (D&6) (D.4 D* (D&8))))) :)
exact Dioph.ext this fun v => matiyasevic.symm
