Moment preservation along the Laurent flow

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 a finite type and $\Gamma=\mathbb F(\iota\sqcup\{*\})$ the free group on $\iota$ and one extra generator $*$; write $c=\lambda(*)$ in $L(\Gamma)$. Let $l:\mathbb Z\to\mathbb C$ be finitely supported with $S=\sum_k l(k)c^k$ self-adjoint, and let $h_j$ ($j\in\iota$) be finitely supported real functions on $\mathbb F(\iota)$. The flow of the paper is the differential equation $\dot X_j=i\Bigl(\sum_g h_j(g)X_gSX_g^*\Bigr)X_j$, where $X_g$ is the evaluation of the word $g$ in the tuple $X$. The flow has a solution $X:\mathbb R\to U(L(\Gamma))^\iota$ with $X_j(0)=\lambda(j)$ such that the tuple $(X(t),c)$ has the same moments as the generators: for all $t\in\mathbb R$ and $g\in\Gamma$,

This is the moment invariance of the flow (Lemma 3.4 of the paper) in the Laurent-polynomial setting.

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.