English
A Diophantine function encodes Pell numbers xn via a constructive Diophantine PFun representation.
Русский
ДиаФантова функция кодирует числа Pелля x_n через конструктивное представление Diophantine PFun.
LaTeX
$$$$\\mathrm{Dioph}\\;\\bigl(\\lambda v. \\text{Pn}\\;\\text{xn}(v_1)=v_2\\bigr).$$$$
Lean4
theorem xn_dioph : DiophPFun fun v : Vector3 ℕ 2 => ⟨1 < v &0, fun h => xn h (v &1)⟩ :=
have : Dioph fun v : Vector3 ℕ 3 => ∃ y, ∃ h : 1 < v &1, xn h (v &2) = v &0 ∧ yn h (v &2) = y :=
let D_pell := pell_dioph.reindex_dioph (Fin2 4) [&2, &3, &1, &0]
(D∃) 3 D_pell
(diophPFun_vec _).2 <| Dioph.ext this fun _ => ⟨fun ⟨_, h, xe, _⟩ => ⟨h, xe⟩, fun ⟨h, xe⟩ => ⟨_, h, xe, rfl⟩⟩
