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.