Local approximation inside the orbit at infinite rank

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$. Tuples carry the metric $\mathrm{dist}(V,U)=\max_i\|V_i-U_i\|$ in the operator norm. Assume that for every $\tau$-preserving automorphism $\Phi$, finite $s\subset\mathrm{Index}$ and $\theta>0$ there are $V$ in the orbit with $\mathrm{dist}(V,\Phi(A))<\theta$ and words $w_j\in\mathbb F_3$ with $\|V_{w_j}-\Phi(\lambda(j))\|_2<\theta$ for all $j\in s$. Then for every $U$ in the orbit, $\delta,\varepsilon>0$ and $g\in\mathbb F(\mathrm{Index})$, there are $V$ in the orbit with $\mathrm{dist}(V,U)<\delta$ and a finitely supported $p:\mathbb F_3\to\mathbb C$ with

This reduces density at infinite rank to finitely many generators at a time.

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.