Q:

Proving a function is primitive recursive

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.  

A:

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.