Lemma: Two properties used below

An admissible compact kernel of the form $P_m$ in a scalar slot represents zero in $\mathcal{W}/\mathcal{J}$. Every element of $\mathcal{J}$ has zero normal symbol on every smooth solution pair

Therefore a normal polynomial with a nonzero value on one such pair is not in $\mathcal{J}$.

Proof. The first statement is the slotwise equation relation. When an equation generator is Wick-multiplied by any functional, all contractions with that generator vanish because the Wick matrix is a bisolution. The product is consequently its ordinary normal-symbol product, which vanishes on the free shell. The same holds for admissible completed slotwise images, by continuity of distributional pairing with fixed smooth configurations. This proves the final separation criterion.