Regular Wick-star contractions are well defined and associative

For each $k$, [F2] constructs $W^{\otimes k}$ on the independent variable pairs. The kernels $F^{(k)}(\varphi )$ and $G^{(k)}(\varphi )$ in [F1] are smooth and compactly supported, so the displayed pairing is defined. In each homogeneous term of $F$ and $G$, pairing the $k$ contracted variables leaves a smooth compact kernel in the remaining variables: the support lies in the projection of the original compact coefficient supports, and [F3] passes every remaining-variable derivative through the pairing. The raw remaining-variable kernel need not be symmetric under permutations exchanging a variable from the $F$ block with one from the $G$ block. For each output degree $r$, replace it by its full symmetrization ${\mathrm{Sym}}_{r}h=\frac{1}{r!}{\sum }_{\pi \in S_r}h(x_{\pi (1)},\dots ,x_{\pi (r)})$. This preserves smoothness and compact support, and its field evaluation is unchanged because both the product ${\prod }_{j=1}^r\varphi (x_j)$ and the product integration measure are invariant under permutations. The resulting symmetric coefficient therefore represents each summand in ${\mathcal{P}}_{\mathrm{r}\mathrm{e}\mathrm{g}}(X)$.

If $F$ and $G$ have degrees $m$ and $n$, then $F^{(k)}=0$ for $k>m$ and $G^{(k)}=0$ for $k>n$. Hence only $0\le k\le \min (m,n)$ contribute; the sum is finite, independent of a coefficient presentation by [F1], and belongs to ${\mathcal{P}}_{\mathrm{r}\mathrm{e}\mathrm{g}}(X)[\eta ]$.

For $f\in \mathcal{D}(X)$, define the auxiliary formal generator by $E_f(s,\varphi ):={\sum }_{m\ge 0}{s}^m{\mathrm{\ell }}_f(\varphi {)}^m\mathrm{/}m!$ in the formal power-series ring; it is not asserted to be an element of ${\mathcal{P}}_{\mathrm{r}\mathrm{e}\mathrm{g}}(X)$. For a zero-constant formal series $Z$, $\exp Z$ means ${\sum }_{r\ge 0}{Z}^r\mathrm{/}r!$, with all equalities interpreted coefficientwise. The $k$-th derivative of $E_f$ in $\varphi$ is $s^k{f}^{\otimes k}{E}_f$. Substitution into the finite coefficient formula gives, coefficientwise in $s,t,\eta$, $E_f(s){\star }_W{E}_g(t)=\exp \text{\hspace{0.17em}⁣}(\eta stW(f,g))E_{sf+tg}\mathrm{.}$

Applying step 2.2 twice, both bracketings of three generators equal $\exp \text{\hspace{0.17em}⁣}(\eta (stW(f,g)+srW(f,h)+trW(g,h)))E_{sf+tg+rh},$ by bilinearity of $W$. Comparing coefficients of $s,t,r$ proves associativity for powers of linear functionals. For distinct tests in one input, replace $f$ by ${\sum }_{j=1}^m{s}_j{f}_j$ in the same coefficientwise identity; its coefficient of $s_1\cdots s_m$ is the symmetrized product ${\mathrm{\ell }}_{f_1}\cdots {\mathrm{\ell }}_{f_m}$. Make this substitution independently in each of the three inputs. Thus the associator vanishes for every symmetrized elementary tensor-product coefficient kernel and for their finite sums.

By [F1], symmetrized finite product-test kernels are dense in every coefficient test space. Each fixed coefficient of the associator is a finite sum of compositions of continuous tensor-distribution pairings from [F2] and smooth parameter pairings from [F3], hence is continuous in the coefficient kernels. Passing to the limits of the product-test approximants from the preceding coefficient comparison proves associativity for arbitrary $F,G,H\in {\mathcal{P}}_{\mathrm{r}\mathrm{e}\mathrm{g}}(X)$.

For linear functionals only $k=0,1$ occur. The $k=0$ term cancels in the commutator, while the $k=1$ terms are $\eta W(f,g)$ and $\eta W(g,f)$; this gives the displayed commutator. If $W$ is Hermitian, conjugating each finite contraction reverses its two variable groups and gives $(F{\star }_{W}G{)}^{\ast }=G^{\ast }{\star }_W{F}^{\ast }$.