# Does a certain mathematical property holds for floating point numbers?

Definitions

Let $\mathbb{F}$ be the set of floating point numbers in a given format, which could be either IEEE-754 binary32 (single precision) or binary64 (double precision).

Let $m(Z)$ the floating point number obtained rounding the real number $Z$.

Let $\phi(Z)$ the next floating point number greater than $Z$.

Let $\lfloor Z \rfloor$ be truncation to 64 bit unsigned integer of the positive floating point number $Z < 2^{64}$ (i.e. there are no overflow concerns).

Hypothesis

Given three numbers $X, Y, A$, such that: $$X, Y, A \in \mathbb{F} \\ 0<X<Y \\ A > m \left( \frac{1}{m(Y-X)} \right) \\ \lfloor m(A\cdot X) \rfloor < \lfloor m(A\cdot Y) \rfloor$$

Question

Is it always true that? $$\lfloor m(\phi(A)\cdot X) \rfloor < \lfloor m(\phi(A)\cdot Y) \rfloor$$

Explanation on the Question

The function $\lfloor m(z\cdot X) \rfloor$ is non-decreasing in $z$ and its behavior is stepwise constant (it looks like a ladder). Increasing $z$ by a tiny bit, the results either does not change, or it jumps to a greater unit.

I am asking if it is possible that by increasing $z$ the terms in the left hand side and right hand side always jump together, or if it is possible that only the term in left hand side jumps befor than the right one, so locally breaking the inequality.

Type of Answer Sought

Either a formal proof that it holds (or that it doesn't), or a numerical example where it does not hold (either in single or double precision) would be accepted as an answer.