The substitution lemma for Scott complexity of finite-rank trees

Let $m\geq 1$. Write $\mathcal{A}_{m+1}$ for the canonical tree of rank $m+1$, and let $B^{(m)}_j:=[m+1:j]$ be the tree obtained by deleting all but $j$ of the level-one subtrees of type $[m:\omega]$. Thus $B^{(m)}_j\not\cong\mathcal{A}_{m+1}$. A root of a $[m:\omega]$-subtree may be relocated to a fresh root of a $[m:k]$-subtree, with witnesses carried to matched witnesses. Substitution lemma, two prongs. For every $m\geq 1$, (a) every $\Pi^{\mathrm{in}}_{2m-1}$ formula true in $\mathcal{A}_{m+1}$ of a tuple consisting of such a root and arbitrary witnesses remains true after relocation for all sufficiently large finite $k$; and (b) for every $\theta\in\Pi^{\mathrm{in}}_{2m}$ and every tuple $\bar a$ satisfying $\mathcal{A}_{m+1}\models\theta(\bar a)$, if $j$ exceeds the number of $[m:\omega]$-roots named by $\bar a$, then $B^{(m)}_j\models\theta(\bar a)$ by re-hosting the inner $\Pi^{\mathrm{in}}_{2m-2}$ witnesses inside $B^{(m)}_j$. Consequently, these two substitution principles should exclude $\Pi^{\mathrm{in}}_{2m+1}$, $\Sigma^{\mathrm{in}}_{2m+1}$, and $\mathrm{d}\text{-}\Sigma^{\mathrm{in}}_{2m+1}$ Scott sentences for $\mathcal{A}_{m+1}$, and yield

$$\operatorname{SSC}(\mathcal{A}_{m+1})=\Pi^{\mathrm{in}}_{2m+2}.$$

This would provide a purely combinatorial proof of the general Scott-complexity theorem, without computability, and would localize the non-$\Sigma^{\mathrm{in}}_{2m}$-definable orbit at $O^m_\omega$. The program is stated to remain open for $m\geq 2$.