A support-explicit normal-jet theorem

For a smooth multiplier $c$, the Leibniz rule gives

Indeed, apply the definition to $c\varphi$ and expand ${{\partial }_q}^{\alpha }(c\varphi )$. This checks the signs in the smooth version of (eq:reference). The distributional cross-line trace version remains the source theorem, with its own microlocal hypotheses.