English
Inverse of Gödel's beta function: unbeta(l) yields a natural number whose beta-coordinates recover the list l.
Русский
Обратная к β-функции: unbeta(l) даёт натуральное число, чьи координаты β восстанавливают список l.
LaTeX
$$$\\beta(\\mathrm{unbeta}(l), i) = l[i]$ for $i$ in Fin(l.length)$$
Lean4
/-- Inverse of Gödel's Beta Function. This is similar to `Encodable.encodeList`, but it is easier
to prove that it is arithmetically definable. -/
def unbeta (l : List ℕ) : ℕ :=
(chineseRemainderOfFinset (l[·]) (coprimes (l[·])) Finset.univ (by simp [coprimes])
(by simpa using Set.pairwise_univ.mpr (pairwise_coprime_coprimes _)) :
ℕ).pair
(supOfSeq (l[·]))!
