English
Nat.binCast is a definitional, binary-representation based embedding of natural numbers into R, defined by binCast(0) = 0 and binCast(n+1) = 2·binCast((n+1)/2) or 2·binCast((n+1)/2) + 1 depending on parity.
Русский
Nat.binCast задаёт отображение натуральных чисел в R по двоичному представлению: binCast(0)=0; binCast(n+1)=2·binCast((n+1)/2) либо 2·binCast((n+1)/2)+1 в зависимости от паритетности (n+1).
LaTeX
$$$\mathrm{Nat.binCast}\colon \mathbb{N} \to R,\quad \mathrm{binCast}(0)=0,\quad \mathrm{binCast}(n+1)=\begin{cases} \mathrm{binCast}((n+1)/2)+\mathrm{binCast}((n+1)/2), & (n+1) \equiv 0 \pmod 2, \\ \mathrm{binCast}((n+1)/2)+\mathrm{binCast}((n+1)/2)+1, & \text{otherwise}.\end{cases}$$$
Lean4
/-- Computationally friendlier cast than `Nat.unaryCast`, using binary representation. -/
protected def binCast [Zero R] [One R] [Add R] : ℕ → R
| 0 => 0
| n + 1 =>
if (n + 1) % 2 = 0 then (Nat.binCast ((n + 1) / 2)) + (Nat.binCast ((n + 1) / 2))
else (Nat.binCast ((n + 1) / 2)) + (Nat.binCast ((n + 1) / 2)) + 1
