 # Projecting real number functions to the naturals

Many useful real number functions, when reduced to natural number functions, become partial. For example, $$f(x) = x / 2$$ is a total function on the real numbers, but not on the naturals. Consider that if $$x = 1,$$ then $$f(x) = 1 / 2,$$ which is not a natural number. It would be ideal to make this function total in some way. It seems likely that defining a function $$g,$$ such that $$g$$ is the integer part of $$f,$$ would be the most useful, so let's do that.

$$g(x) = \begin{cases} 0 & \text{if }x \lt 2 \\ g(x) + 1 & \text{otherwise} \end{cases}$$

and this function quickly generalizes to

$$h(x) = \begin{cases} 0 & \text{if }x \lt k \\ h(x) + 1 & \text{otherwise} \end{cases}$$

Subtraction is decidedly useful. It's total for pairs of real numbers, but not for pairs of naturals. Again, we do our best to maintain the usefulness of this function, while making it total.

$$x \mathop{\dot -} y = \begin{cases} x - y & \text{if }x \ge y \\ 0 & \text{otherwise} \end{cases}$$