Show that floating point √x⋅x≥x\sqrt{x \cdot x} \geq x for all long xx.

I verified experimentally that in Java the equality

Math.sqrt(x*x) = x


holds for all long x such that x*x doesn’t overflow. Here, Java long is a $64$ bit signed type and double is a IEEE binary floating point type with at least $53$ bits mantissa and sufficiently long exponent.

Mathematically, there are two imprecise functions involved:

• Conversion from long to double which loses precision due to the mantissa being only $53$ bits where $63$ bits would be needed. This operation is guaranteed to return the closest representable result.
• Computing square root, which is also guaranteed to return the closest representable result.

Mathematically, this can be expressed like

where $\mathrm{round}$ is the rounding function from $\mathbb R$ into the set of all numbers representable as double.

I’m looking for a proof since no experiment can assure it works across all machines.

The idea is simple: Find upper and lower bounds for

and show that $\mathrm{round}(X) = x$.

Let $\mathrm{ulp}(x)$ denote the unit of least precision at $x$
and let $E(x)$ and $M(x)$ denote the exponent and mantissa of $x$, i.e.,

with $1 \le M(x) < 2$ and $E(x) \in \mathbb Z$. Define

where $\mu=2^{-52}$ is the machine epsilon.

Expressing the rounding function by its relative error leads to

We know that $|\epsilon| \le \frac12\Delta(x^2)$ and get (ignoring the trivial case $x=0$)

By observing $M(x)$ and $M(x^2)$ e.g. over the interval $[1, 4]$,
it can be easily be shown that $\frac{M(x)}{M(x^2)} \le \sqrt2$ which gives us

and therefore

Analogously we get the corresponding lower bound. Just instead of

we use something like

which suffices, since we used a very generous estimate ($\sqrt2/4<\frac12$) in the last step.

Because of $|X-x|$ being smaller than $\frac12 \mathrm{ulp}(x)$, $x$ is the double closest to $X$, therefore $\mathrm{round}(X)$ must equal to $x$, q.e.d.