Symmetric lifting lemma: reflection-closed even completion absorbs an odd target

A tree witness is a function $\theta:\mathbb N\times\mathbb Z\to\{0,1\}$ on the nodes $(k,r)$ of the binary residue tree. 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$. 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. For a word $W$ write $W_0=(x/2 : x\in W \text{ even})$ and $W_1=((x-1)/2 : x\in W\text{ odd})$ for its normalized parity halves (order kept), and let $\theta_c(k,r)=\theta(k+1,2r+c)$ be the shifted witnesses.

Symmetric lifting lemma. Let $\theta$ be a tree witness with $\theta(0,0)=0$ and let $S$ be a $\theta$-safe word. (Safety with $\theta(0,0)=0$ is equivalent to $S$ being safe and released: every open in-order pair $(a,b)$ with $b-a$ odd ends at an even $b$.) Let $R$ be a finite list of even integers and $y\notin S$ an odd integer. Suppose

• the even half $(S\cdot R)_0$ is $\theta_0$-safe,
• the odd half $(S\cdot(y))_1$ is $\theta_1$-safe,
• the even entries $A$ of $S\cdot R$ satisfy $a\in A\Rightarrow 2y-a\in A$.

Then

(and hence again safe and released, with the same witness). The lemma is the positive half of the parity-decomposition analysis of root release in the tree-witness approach to Erdős Problem 195: it reduces absorbing an odd target after a released word to two half-problems plus a reflection-symmetric even completion. Companion results show the symmetric completion need not exist (e.g. from $S=(0,-2)$, $y=1$).

Formalization note: Safe and treeLt come from Definitions.Def_Erdos195_tree; positions are first occurrences (List.idxOf); halves are filter by x % 2 = c followed by map (· / 2) (floor division). No distinctness of the entries of $R$ is assumed.