Lemma: Formal advanced solution

For a formal compact test $d$, the equation

has a unique smooth advanced-type formal solution, where advanced-type means that each coefficient is supported in $J_{\eta }^{-}(K_0)$ for a compact $K_0$. It is

Proof. The coefficient equations are

Each right-hand side is smooth and compact because the $d_j$ and interaction coefficients are compact. Successive application of ${\mathsf{E}}_{\mathrm{A}}$ gives the displayed solution and its causal support.

A homogeneous advanced-type free solution vanishes on a sufficiently late complete flat Cauchy surface, so it vanishes by free Cauchy uniqueness. Induction proves formal uniqueness. Finally $P_m{\mathsf{E}}_{\mathrm{A}}{\mathcal{R}}_{q}d={\mathcal{R}}_{q}d$, since ${\mathcal{R}}_{q}d$ is a formal compact test.