Lemma: Necessary derivative condition

If $F\in {\mathcal{P}}_{\mathrm{mc}}$, then every functional derivative satisfies

at every smooth configuration $\Psi$. In particular, $F^{(1)}(\Psi )$ has no nonzero timelike covector in its wavefront set.

Proof. Differentiation produces finite sums of partial contractions of the compact kernels $u_n$ with smooth configurations. In the wavefront bound for a partial contraction, the covectors in the contracted slots must be zero. If the remaining covectors were all future nonspacelike, or all past nonspacelike, adjoining the zero covectors would give a forbidden element of $\mathrm{WF}(u_n)$. This proves the claim. The same argument applies componentwise in the graded theory.