Extremal-parity lemma for node-consistent words

For a finite word $A$ of integers, an in-order pair $(x,y)$ of $A$ ($x$ occurs before $y$) is open if $2y-x\notin A$ and $3y-2x\notin A$. It lies at the node $(k,\,x\bmod 2^k)$ of the binary residue tree, where $k=\nu_2(y-x)$, and it forces the bit $\mathrm{bit}_k(y)=\lfloor y/2^k\rfloor\bmod 2$ there. The word satisfies SAFE(ii), or node consistency, if no node is forced to both bits by open pairs: any two open pairs at the same node force the same bit. Let $A=(a,b,\dots)$ be a finite word that satisfies SAFE(ii) and whose first two entries have opposite parity. Let $L,U$ be its minimum and maximum, and suppose $L<a<U$. Then

Otherwise the extreme $z$ of parity opposite to $a$ and the other extreme $w$ give open root pairs $(a,z)$ and $(b,w)$, which force opposite root bits. The lemma is a basic constraint on completions in the tree-witness approach to Erdős Problem 195. It rules out symmetric completions about a half-integer.

Formalization note: SAFE(ii) is stated inline exactly as the second conjunct of Erdos195.exists_treeLt_safe_iff. Positions are List.idxOf, $\nu_2$ is padicValInt 2, and $\mathrm{bit}_k$ is bitOne from Definitions.Def_Erdos195_defs. Distinctness of the entries is not needed. The extremes are given as $L,U\in A$ with $L\le x\le U$ for all $x\in A$.