Flow extension with inactive free generators

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 $\iota$ be finite, $\kappa$ arbitrary, and let $M=L(\mathbb F(\iota\sqcup\kappa\sqcup\{*\}))$ with $c=\lambda(*)$. Let $l:\mathbb Z\to\mathbb C$ be finitely supported with $S=\sum_k l(k)c^k$ self-adjoint, let $h_i$ ($i\in\iota$) be finitely supported real functions on $\mathbb F(\iota)$, and let $X:\mathbb R\to U(M)^\iota$ solve $\dot X_i=i\bigl(\sum_g h_i(g)X_gSX_g^*\bigr)X_i$ with $X_i(0)=\lambda(i)$, where $X_g$ is the evaluation of the word $g$ in the tuple $X$. Let $T(t)$ be the tuple consisting of $X_i(t)$ on $\iota$ and $\lambda(k)$ on $\kappa$. For every $t$ there is a $\tau$-preserving ultraweakly continuous $*$-automorphism $\Phi$ of $M$ such that $\Phi(\lambda(g))$ is the evaluation of $g$ in $(T(t),c)$, for every word $g$.

Together with moment preservation, this extends the flow automorphisms of the paper to infinitely many inactive generators.

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.