Local approximation inside the orbit, rank at least two

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 $M=L(\mathbb F(\mathrm{Fin}\,n\sqcup\{*\}))$, and let the orbit be the set of tuples $(\Phi(\lambda(j)))_{j\in\mathrm{Fin}\,n}$ as $\Phi$ runs over the $\tau$-preserving $*$-automorphisms of $M$. For a tuple $V$ of unitaries, $V_g$ is the evaluation of the word $g$ and $\mathrm{poly}(V,p)=\sum_g p(g)V_g$. Tuples carry the metric $\mathrm{dist}(V,U)=\max_j\|V_j-U_j\|$ in the operator norm. Let $n\ge2$. For every $U$ in the orbit, every $\delta,\varepsilon>0$ and every $g\in\mathbb F(\mathrm{Fin}\,n\sqcup\{*\})$ there are $V$ in the orbit with $\mathrm{dist}(V,U)<\delta$ and a finitely supported $p:\mathbb F_n\to\mathbb C$ such that

The paper's Section 5 iteration treats $n\ge3$; this is the rank-at-least-two version of the Lean counterpart of its inductive step: a small move within the orbit brings a word algebra of the tuple close to any prescribed basis vector. In Lean it feeds a Baire-type lemma rather than an explicit iteration.

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.