Parity decomposition of $\varepsilon$-safety

Fix $\varepsilon:\mathbb{N}\to\{0,1\}$ and the $2$-adic total order on $\mathbb{Z}$ given by $x\prec_\varepsilon y$ iff $x\neq y$ and the $k$-th two's-complement digit of $x$ equals $\varepsilon_k$, where $k=\nu_2(y-x)$. A finite word $Q$ of integers is $\varepsilon$-safe if the sequence "the letters of $Q$ in order, then all remaining integers in $\prec_\varepsilon$-order" contains no monotone $4$-term arithmetic progression. Let $\eta_k=\varepsilon_{k+1}$, and for $p\in\{0,1\}$ let $R_p$ be the word obtained from $Q$ by keeping the letters $x\equiv p\pmod 2$, in order, and replacing each by $(x-p)/2$. Then $Q$ is $\varepsilon$-safe if and only if all of the following hold:

So safety splits into the two parity classes (a problem of the same kind one binary digit lower) plus cross-parity conditions that involve only $\varepsilon_0$. This reduces extension and merging questions for Ho-style constructions of $4$-AP-free permutations of $\mathbb{Z}$ (Erdős Problem 195) to the rescaled parity classes.

Formalization note: Safe, epsLt are from Definitions.Def_Erdos195_defs; $R_0$ is (Q.filter (fun x => decide (x % 2 = 0))).map (fun x => x / 2), $R_1$ is the analogue with (x - 1) / 2; "precedes" is comparison of List.idxOf; condition (4) is stated as b % 2 = 1 ↔ ε 0 = true.