English
Let unpair be the natural number to pair map: there is a rule using s = floor(sqrt(n)) that assigns to n a unique pair (a,b) of natural numbers, namely a = n − s^2 and b = s if n − s^2 < s, otherwise a = s and b = n − s^2 − s. This provides a canonical way to encode pairs as a single natural number.
Русский
Пусть существует распаковочная функция unpair: каждому натуральному числу n сопоставляется пара (a, b) натуральных чисел так, что при s = ⌊√n⌋ выполняется либо (a, b) = (n − s^2, s), либо (a, b) = (s, n − s^2 − s). Это единственный способ кодирования пары в одно число.
LaTeX
$$$ \operatorname{unpair}(n) = \begin{cases} (n - s^2,\; s), & n - s^2 < s, \\ (s,\; n - s^2 - s), & \text{otherwise} \end{cases}, \quad s = \sqrt{n}. $$$
Lean4
/-- Unpairing function for the natural numbers. -/
@[pp_nodot]
def unpair (n : ℕ) : ℕ × ℕ :=
let s := sqrt n
if n - s * s < s then (n - s * s, s) else (s, n - s * s - s)
