Localization: a safe extension inside one residue class lifts to the whole tree-safe word

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$. For letters $x$ before $z$ in $Q$, the pair $(x,z)$ is OPEN if neither $2z-x$ nor $3z-2x$ occurs in $Q$; it sits at the node $(h,\,x\bmod 2^h)$, $h=\nu_2(z-x)$, and forces the digit $\mathrm{bit}_h(z)$ there.

Theorem (localization). Let $Q$ be SAFE, fix a residue class $C=\rho+2^k\mathbb Z$, and let $D$ be a finite word of letters of $C$ none of which occurs in $Q$. Let $Q_C$ be the subsequence of $Q$ consisting of its letters in $C$. Assume

1. the local word $Q_C\cdot D$ is SAFE, and
2. (ancestor compatibility) every OPEN pair $(x,z)$ of $Q$ sitting at an ancestor node $(h,\rho\bmod 2^h)$ with $h<k$ forces $\mathrm{bit}_h(z)=\mathrm{bit}_h(\rho)$.

Then

So a finite safe extension built locally inside one residue class transfers to the whole word, and no new conflict appears at a node shallower than $k$. Combined with local absorption recipes (one or two local letters, or a one-grandchild block), it gives target-last absorption inside arbitrary larger safe words.

Formalization note: treeLt θ is from Definitions.Def_Erdos195_tree, and Safe is from Definitions.Def_Erdos195_defs. $Q_C$ is Q.filter (fun x => decide (x % 2 ^ k = ρ % 2 ^ k)), and positions are List.idxOf.