Absorbing any extra generator from the distinguished one

Throughout, $L(G)$ is the group von Neumann algebra of a discrete group $G$ acting on $\ell^2(G)$, with canonical trace $\tau(x)=\langle x\delta_e,\delta_e\rangle$, left-regular unitaries $\lambda(g)$, and $\|x\|_2=\|x\delta_e\|_{\ell^2}$. Let $\mathrm{Index}=\mathrm{Fin}\,3\sqcup\mathbb N\sqcup\{*\}$ and $M=L(\mathbb F(\mathrm{Index}))$. Let $A_i=\lambda(i)$ for $i\in\mathrm{Fin}\,3$ be the initial tuple, and for $q\in\mathbb N\sqcup\{*\}$ let $E_q=\lambda(q)$ be the extra generators. The orbit is the set of tuples $(\Phi(A_i))_i$ for $\tau$-preserving $*$-automorphisms $\Phi$ of $M$. Assume that for every $\varepsilon>0$ there are a $\tau$-preserving automorphism $\alpha$ fixing each $E_k$, $k\in\mathbb N$, and a word $w\in\mathbb F_3$ with $\|\alpha(A_i)-A_i\|<\varepsilon$ and $\|\alpha(A_w)-E_*\|_2<\varepsilon$. Then for every $q$ and $\varepsilon>0$ there are a $\tau$-preserving automorphism $\alpha$ fixing each $E_r$, $r\ne q$, and a word $w\in\mathbb F_3$ with

This reduces the absorption of an arbitrary extra generator to the distinguished one.

Formalization Note The statement is verbatim from OpenAI's Lean development, with the listed Definitions imported in place of the upstream modules; the definitions are supporting code for this statement.