English
If f and g are DiophFn, then the function v ↦ f(v)^{g(v)} is Diophantine (Matiyasevic-type result).
Русский
Если f и g — диофантовы функции, тогда f(v)^{g(v)} диофантова (результат Матиясевича-type).
LaTeX
$$$$\\forall {f,g:(\\alpha\\to\\mathbb{N})\\to \\mathbb{N},\\; \\mathrm{DiophFn}\\,f \\to \\mathrm{DiophFn}\\,g \\to \\mathrm{DiophFn}\\bigl(\\lambda v. f(v)^{g(v)}\\bigr).$$$$
Lean4
/-- A version of **Matiyasevic's theorem** -/
theorem pow_dioph {f g : (α → ℕ) → ℕ} (df : DiophFn f) (dg : DiophFn g) : DiophFn fun v => f v ^ g v :=
by
have :
Dioph
{v : Vector3 ℕ 3 |
v &2 = 0 ∧ v &0 = 1 ∨
0 < v &2 ∧
(v &1 = 0 ∧ v &0 = 0 ∨
0 < v &1 ∧
∃ w a t z x y : ℕ,
(∃ a1 : 1 < a, xn a1 (v &2) = x ∧ yn a1 (v &2) = y) ∧
x ≡ y * (a - v &1) + v &0 [MOD t] ∧
2 * a * v &1 = t + (v &1 * v &1 + 1) ∧
v &0 < t ∧ v &1 ≤ w ∧ v &2 ≤ w ∧ a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1)} :=
(D&2 D= D.0 D∧ D&0 D= D.1) D∨
(D.0 D< D&2 D∧
((D&1 D= D.0 D∧ D&0 D= D.0) D∨
(D.0 D< D&1 D∧
((D∃) 3 <|
(D∃) 4 <|
(D∃) 5 <|
(D∃) 6 <|
(D∃) 7 <|
(D∃) 8 <|
pell_dioph.reindex_dioph (Fin2 9) [&4, &8, &1, &0] D∧
( D≡ (D&1) (D&0 D* (D&4 D- D&7) D+ D&6) (D&3)) D∧
D.2 D* D&4 D* D&7 D= D&3 D+ (D&7 D* D&7 D+ D.1) D∧
D&6 D< D&3 D∧
D&7 D≤ D&5 D∧
D&8 D≤ D&5 D∧
D&4 D* D&4 D-
((D&5 D+ D.1) D* (D&5 D+ D.1) D- D.1) D* (D&5 D* D&2) D* (D&5 D* D&2) D=
D.1))) :)
exact
diophFn_comp2 df dg <|
(diophFn_vec _).2 <|
Dioph.ext this fun v =>
Iff.symm <|
eq_pow_of_pell.trans <|
or_congr Iff.rfl <|
and_congr Iff.rfl <|
or_congr Iff.rfl <|
and_congr Iff.rfl <|
⟨fun ⟨w, a, t, z, a1, h⟩ => ⟨w, a, t, z, _, _, ⟨a1, rfl, rfl⟩, h⟩,
fun ⟨w, a, t, z, _, _, ⟨a1, rfl, rfl⟩, h⟩ => ⟨w, a, t, z, a1, h⟩⟩
