Proving a function is primitive recursive

Question

Let f(z) be the integer j such that $j \le (1+ \sqrt2) \times z < j+1$. Show f(z) is primitive recursive.

Attempt: I am having a lot of trouble with $\sqrt 2$. Unable to compute it. How could you do that? I am able to come up with a definition for $ \lfloor \sqrt x \rfloor$.

Here $\dot{-}$ is only defined when x $\ge$ y else it is 0.

$\mbox{$\lfloor \sqrt {x+1} \rfloor$ } = \begin{cases} \lfloor \sqrt x \rfloor + sg(( \lfloor \sqrt x \rfloor + 1)^2 \dot{-} (x+1)) , & \text{if } x \neq 0,\\ 0, & \text{if } x = 0. \end{cases} \qquad $ $\mbox{sg}(x) = \begin{cases} 1, & \text{if } x \neq 0,\\ 0, & \text{if } x = 0. \end{cases} \qquad \overline{\mbox{sg}}(x) = 1\ \dot{-}\ \mbox{sg}(x),$

https://en.wikipedia.org/wiki/Primitive_recursive_function

Also assume I can compute the least value $i \le y$ for which a predicate is true. That definition I have already read. Also summation, product, bounded quantifiers are primitive recursive. I want to compute this f(x) in terms of these known primitive recursive functions.

Answer 1

We can describe $f(z)$ as the largest $j$ such that $j\le(1+\sqrt2)z<j+1$. If we try $j=z$, we certainly have $j\le(1+\sqrt2)z$, so for $f(z)$ we need only consider $j\ge z$. If $j\ge z$, then

$$\begin{align*} (1+\sqrt2)z<j+1&\text{ iff }j+1-z>z\sqrt2\\ &\text{ iff }(j+1-z)^2>2z^2\\ &\text{ iff }(j+1-z)^2\mathrel{\dot-}2z^2\ne 0\;, \end{align*}$$

and $(j+1-z)^2$ is monotonically increasing in $j\ge z$. Let $j_0$ be the least $j\ge z$ such that

$$(j+1-z)^2\mathrel{\dot-}2z^2\ne 0\;;$$

this is the least $j\ge z$ such that $(1+\sqrt2)z<j+1$, which is exactly what we want.