Absolute Value Inequalities

The following question arose today: given divisible variables $x,y\in(-\infty,+\infty)$, how does one implement in a mathematical program the constraint $|x|\le|y|$?

To start, I do not think it can be done with unbounded variables. Then again, I'm not a big believer in unbounded variables in practice. (Physicists seem to believe the number of atoms in the universe is finite, which gives us a starting point at bounding all physical variables. They also believe the universe will eventually suffer heat death, which gives us a start at bounding time variables.)

Let us assume instead that $L_{x}\le x\le U_{x}$ and $L_{y}\le y\le U_{y}$, with no restrictions on which bounds are positive or negative. Now add a binary variable $z$, which will take value 0 if $y$ is positive and 1 if $y$ is negative.  We enforce that with the constraints\begin{eqnarray*}y & \le & U_{y}\times(1-z)\\y & \ge & L_{y}\times z.\end{eqnarray*} [LaTeXMathML does not support equation numbering, so please number the inequalities above (1) and (2) mentally, and the inequalities below (3)--(6). Sorry about that!] Note that the value of $z$ is undetermined if $y=0$, which will not be a problem. Now add the constraints\begin{eqnarray*} x & \le & y+\left(U_{x}-L_{y}\right)\times z\\ -x & \le & y-\left(L_{x}+L_{y}\right)\times z\\ x & \le & -y+\left(U_{y}+U_{x}\right)\times\left(1-z\right)\\ -x & \le & -y+\left(U_{y}-L_{x}\right)\times\left(1-z\right).\end{eqnarray*} If $y>0$, then (1) forces $z=0$, in which case (5) and (6) become vacuous (since $x\le U_{x}\le U_{x}+(U_{y}-y)$ and $-x\le-L_{x}\le-L_{x}+(U_{y}-y)$ respectively). Meanwhile, (3) and (4) become $x\le y$ and $-x\le y$, which enforces $|x|\le y=|y|$. Similarly, if $y<0$, then (2) forces $z=1$, which makes (3) and (4) vacuous and turns (5) and (6) into $x\le-y$ and $-x\le-y$, so that $|x|\le-y=|y|$. Finally, if $y=0$, then it does not matter whether $z=0$ or $z=1$, since either (3) and (4) (if $z=0$) or (5) and (6) (if $z=1$) will force $x=0$.