beta — Mathlib

English

Gödel's beta function β(n,i) is defined via a standard pairing: if n unpairs to (a,b), then β(n,i) = a mod ((i+1)b + 1).

Русский

Гёделева β-функция β(n,i) задаётся через разложение n на пару (a,b): β(n,i) = a mod ((i+1)b + 1).

LaTeX

$$$\\beta(n,i) = \\text{fst}(\\mathrm{unpair}(n)) \\bmod ((i+1)\\text{snd}(\\mathrm{unpair}(n)) + 1)$$$

Lean4

/-- Gödel's Beta Function. This is similar to `(Encodable.decodeList)[i]`, but it is easier to
prove that it is arithmetically definable. -/
def beta (n i : ℕ) : ℕ :=
  n.unpair.1 % ((i + 1) * n.unpair.2 + 1)

Похожие утверждения