Exact lifting criterion: absorbing an odd target after an even batch, with odd fourth-term helpers

A tree witness is a function $\theta(k,r)\in\{0,1\}$ on the nodes $(k,r)$, $0\le r<2^k$, 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)=\theta(k,\,x\bmod 2^k)$. A finite word $Q$ of integers is $\theta$-safe if the sequence "the letters of $Q$ in order, then all remaining integers in $\prec_\theta$-order" contains no monotone $4$-term arithmetic progression. The halves of a word are the subsequences of its even letters and of its odd letters, each mapped by $x\mapsto\lfloor x/2\rfloor$. The half witnesses are $\theta_E(k,r)=\theta(k+1,2r)$ and $\theta_O(k,r)=\theta(k+1,2r+1)$.

Theorem (exact lifting criterion). Let $\theta(0,0)=0$ ("released" root). Let $S$ be a $\theta$-safe word, $R$ a word of even integers, and $y\notin S$ an odd integer. Write $P=S\cdot R$. Then $S\cdot R\cdot y$ is $\theta$-safe if and only if

1. the even half of $P$ is $\theta_E$-safe,
2. the odd half of $S\cdot y$ is $\theta_O$-safe, and
3. every even letter $a$ of $P$ satisfies

This sharpens the symmetric lifting lemma, where every even letter is reflected ($2y-a\in P$), into an exact characterization. An even letter may instead be covered by an odd fourth-term helper $3y-2a$ that is already in $S$, provided the odd letter $2a-y$ does not precede it. So absorbing an odd target after an even batch into a released safe word reduces exactly to two half-safety problems plus this local helper condition.

Formalization note: treeLt θ is from Definitions.Def_Erdos195_tree, and Safe is from Definitions.Def_Erdos195_defs. Halves are filter by parity followed by map (· / 2). Positions are List.idxOf.