$\varepsilon$-orders contain no monotone $3$-term AP

For every $\varepsilon$, there are no integers $a$ and $r\neq0$ with

Since $r$ may be negative, this excludes both increasing and decreasing $3$-term progressions in $\prec_\varepsilon$ order. This is the $\mathbb{Z}$-version of the $3$AP-freeness of Ho's order $\triangleleft$.

Formalization Note epsLt ε x y is x ≠ y ∧ (x / 2^k % 2 = 1 ↔ ε k = true) with k = padicValInt 2 (y - x), i.e. $k=\nu_2(y-x)$; integer division is floor division, so x / 2^k % 2 is the $k$-th two's-complement digit of $x$.