Tree-safe repair of $P_n\cdot T$ needs at least $n$ auxiliary letters

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)$ (two's-complement digits). 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. Let $n\ge0$, $N=2^n$, $T=4N$. Let $Q$ be a $\theta$-safe word (any tree witness $\theta$) with $T\in Q$ and $N\notin Q$, such that for every $k<n$ the letters $N-2^{k+1}$, $N-2^k$, $2^k$ occur in $Q$, with $N-2^{k+1}$ before $N-2^k$ and $2^k$ before $T$. Then for every $k<n$

The hypotheses hold for every word that begins with $P_n=\{0,1,\dots,N-1\}$ listed in increasing $\prec_0$-order (the order with all digits preferred $0$) and contains $T$ but not $N$: the pairs $(N-2^{k+1},N-2^k)$ and $(2^k,T)$ sit at the same tree node $(k,0)$ and force opposite values there. So absorbing the single new target $T$ into $P_n$ by tree-safe insertion needs at least $n$ auxiliary letters: there is no uniform bound on the repair cost (Erdős Problem 195, tree-witness approach).

Formalization note: treeLt θ is from Definitions.Def_Erdos195_tree; Safe from Definitions.Def_Erdos195_defs; positions are List.idxOf; the count is the cardinality of Q.toFinset filtered by $x\notin[0,N)$, $x\ne T$. The word $P_n$ itself is not formalized; the theorem assumes only the order relations it uses.