Why upper support bounds do not prove the bridge

For the sharp insertion, the metric variation is

Set $a_{\mu }=-f{\partial }_{\mu }\varphi$ and $b={\mathsf{E}}_0^{\ast }a$, in the inherited adjoint convention. Its metric derivative is represented by the full distribution

The scalar variation remains

Lemma lem:derivative-support therefore identifies what a lower support proof must examine. It does not evaluate those supports. Such a proof must control the actual bulk distribution, its surface trace, all allowed scalar gradients, and possible cancellations. A nonzero candidate cone, or the support of one formal summand, does not by itself establish nonzero dependence of the complete functional.

The surface term cannot be discarded, and the on-shell smoothing cannot replace it. Actual-presentation cancellations must also be respected: support belongs to the functional, not to a chosen test presentation.