Reflection absorption for a one-grandchild block: $(a,B,2y-B,y)$ is tree-safe

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; $Q$ is SAFE if it is $\theta$-safe for some $\theta$.

Theorem (reflection absorption for a one-grandchild block). Let $a\in\mathbb Z$, $k\ge 0$, and let $B=(b_1,\dots,b_m)$ be a finite word such that $a\cdot B$ is SAFE. Suppose that

• $\nu_2(b-a)=k$ for every $b\in B$ (so $a$ and $B$ lie in the same class mod $2^k$ but in opposite classes mod $2^{k+1}$),
• all entries of $B$ are congruent modulo $2^{k+2}$ (one grandchild), and
• $y\ne a$ and $y\equiv a \pmod{2^{k+1}}$.

Then the word

is SAFE. Thus the target $y$ is absorbed last, using exactly $|B|$ auxiliary letters (the reflection of $B$ about $y$, in the original order).

Formalization note: treeLt θ is from Definitions.Def_Erdos195_tree, and Safe is from Definitions.Def_Erdos195_defs. The hypotheses are stated with divisibility: $2^k\mid b-a$ and $2^{k+1}\nmid b-a$; $2^{k+2}\mid b'-b$; $2^{k+1}\mid y-a$. a :: B ++ L parses as (a :: B) ++ L.