Parity decomposition of tree-witness safety (two half-scale problems plus a root condition)

A tree witness is a function $\theta:\mathbb N\times\mathbb Z\to\{0,1\}$ on the nodes $(k,r)$ of the binary tree of residues. For distinct integers $x,y$ with $k=\nu_2(y-x)$, put $x\prec_\theta y$ iff $\mathrm{bit}_k(x)=1 \Leftrightarrow \theta(k,\,x\bmod 2^k)=1$ ($\mathrm{bit}_k$ is the $k$-th two's-complement binary digit). A finite word $Q$ of integers is $\theta$-safe if the completion "the letters of $Q$ in order, then all remaining integers in $\prec_\theta$-order" contains no monotone $4$-term arithmetic progression (positions of $a,a+r,a+2r,a+3r$ increasing, $r\neq0$). Positions in $Q$ are first occurrences. For a word $Q$ let $Q_0$ be the subsequence of even letters mapped by $x\mapsto x/2$, and $Q_1$ the subsequence of odd letters mapped by $x\mapsto (x-1)/2$. Let $\theta_c(k,r)=\theta(k+1,\,2r+c)$ for $c\in\{0,1\}$. Then

where the root condition (R) says: for every pair $a,b\in Q$ with $b-a$ odd and $a$ before $b$, (i) if $2b-a\in Q$ occurs after $b$ then $3b-2a\in Q$ occurs before $2b-a$; (ii) if neither $2b-a$ nor $3b-2a$ lies in $Q$ then $b$ is odd exactly when $\theta(0,0)=1$.

This is the exact self-similarity of tree safety: all non-root constraints split into two independent problems of the same kind one binary digit lower (for the two subtrees of $\theta$), and the halves interact only through the odd-difference root condition (R). It generalizes the parity decomposition for $\varepsilon$-orders (the case $\theta(k,r)=\varepsilon_k$).

Formalization note: treeLt, Safe, bitOne from Definitions.Def_Erdos195_tree/Def_Erdos195_defs; positions are List.idxOf; x / 2 is floor division, so it equals $(x-1)/2$ on odd $x$.