Freely generating Haar tuple of rank n in L(F_{n+1}), n at least three

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 $n\ge3$ and $M=L(\mathbb F(\mathrm{Fin}\,n\sqcup\{*\}))$. There is an $n$-tuple $U$ of unitaries in $M$ with $\tau(U_g)=0$ for every nonidentity $g\in\mathbb F_n$, and such that the vectors $U_g\delta_e$ have dense linear span in $\ell^2(\mathbb F(\mathrm{Fin}\,n\sqcup\{*\}))$:

This plays the role of the limit tuple constructed in the proof of Theorem 1.1 of the paper, and Lean obtains it by a Baire-type lemma rather than an explicit iteration; Lemma 2.2 then gives $L(\mathbb F_n)\cong L(\mathbb F_{n+1})$.

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.