@Jonathan:

> (It seems clear that requiring multiplication on both sides to preserve the order is equivalent to requiring \\((x, x') \le (y, y') \implies x \otimes y \le x' \otimes y'\\).

Right! If \\(x\leq x'\\) and \\(y\leq y'\\), then we get \\(x\otimes y\leq x\otimes y'\leq x'\otimes y'\\), which means that it's enough to postulate each one of these two inequalities separately. So indeed the answer to my puzzle is 'yes' in the commutative case for exactly this reason.

Concerning the noncommutative case, I also like your new hunch ;)

> (It seems clear that requiring multiplication on both sides to preserve the order is equivalent to requiring \\((x, x') \le (y, y') \implies x \otimes y \le x' \otimes y'\\).

Right! If \\(x\leq x'\\) and \\(y\leq y'\\), then we get \\(x\otimes y\leq x\otimes y'\leq x'\otimes y'\\), which means that it's enough to postulate each one of these two inequalities separately. So indeed the answer to my puzzle is 'yes' in the commutative case for exactly this reason.

Concerning the noncommutative case, I also like your new hunch ;)