Proposition: Zero-charge comparison classes

At every smooth configuration and after every finite smooth directional insertion,

Proof. For $Q,Q^R$, every nonzero remaining metric kernel is compact smooth, as in Proposition prop:firstcontinuity.

For $F\in {\mathcal{P}}_{\mathrm{mc}}$, contraction of higher functional derivatives with smooth directions is a proper pushforward after compact cutoffs on the coefficient supports. A wavefront covector of the remaining metric slot would come from a joint covector with all integrated slots zero. A nonzero causal covector there would make that joint covector entirely future or entirely past causal, excluded by the old microcausal condition. The remaining kernel therefore avoids causal covectors. It belongs to ${\mathcal{S}}_1$ by adapted admission, so Lemma lem:MCcharge applies.