IEEE double such that sqrt(x*x) ≠ x

Does there exist an IEEE double x>0 such that sqrt(x*x) ≠ x, under the condition that the computation x*x does not overflow or underflow to Inf, 0, or a denormal number?

This is given that sqrt returns the nearest representable result, and so does x*x (both as mandated by the IEEE standard, "square root operation be calculated as if in infinite precision, and then rounded to one of the two nearest floating-point numbers of the specified precision that surround the infinitely precise result").

Under the assumption that if such doubles would exist, then there are probably examples close to 1, I wrote a program to find these counterexamples, and it failed to find any between 1.0 and 1.0000004780981346.

The previous similar question perfect squares and floating point numbers answers the question in the negative for situations where the computation of x*x does not involve rounding. That answer is not sufficient for this question because it may be possible for x*x to involve rounding in one direction, then sqrt(x*x) to involve rounding in the same direction, thus producing an answer that is not exactly x.

Sylvie Boldo has formally proved that a floating-point number satisfying the conditions in your question does not exist.

Quoting the abstract of the article:

Floating-point experts know that mathematical formulas may fail or give imprecise results when implemented in floating-point arithmetic. This article describes an example where, surprisingly, it is absolutely not the case. Indeed, using radix 2 and an unbounded exponent range, the computation of the square root of the square of a floating-point number a is exactly |a|. A consequence is the fact that the floating-point computation of a/ sqrt (a² + b²) is always in the interval [−1, 1]. This removes the need for a test when calling an arccos or an arcsin on this value. For more guarantees, this property was formally checked using the Coq proof assistant and the Flocq library. The conclusion will give hints on what happens without assumptions and in other radices, where the behavior is very different.

“using radix 2” was likely implicit in your question (although the IEEE has also standardized decimal floating-point number formats and operations), and “an unbounded exponent range” is equivalent to your “no overflow or underflow” restriction.

A reason making the property possible at all is that x*x “expands” (the interval [1,2] is mapped to [1,4], for instance) in a way such that, when there is no overflow or underflow, the rounding that can happen for * is benign and x is still the closest representable floating-point number to the real square root of the floating-point product x*x. This hand-wavy argument does not constitute a proof, so it's a good thing that the article linked above contains one.