Let $X$ be a smooth manifold and let $m,s \in \mathbb{R}$. Let $P \in \Psi^m(X)$ be a properly supported classical pseudodifferential operator with scalar real homogeneous principal symbol $p_m:T^*X \setminus 0 \to \mathbb{R}$. Let $q_0 \in \operatorname{Char}(P)=p_m^{-1}(0)$, and assume that $H_{p_m}(q_0) \neq 0$. Let $\Sigma \subset \operatorname{Char}(P)$ be a smooth conic hypersurface through $q_0$ transverse to $H_{p_m}$; it is used only to choose a local conic transversal to the Hamilton flow. Let $\gamma:(-\varepsilon,\varepsilon) \to \operatorname{Char}(P)$ be the bicharacteristic of $H_{p_m}$ satisfying $\gamma(0)=q_0$, oriented so that $\dot{\gamma}(t)=H_{p_m}(\gamma(t))$.

Assume that, after replacing $\varepsilon$ by a smaller positive number, there is a conic neighbourhood $\Omega \subset T^*X\setminus 0$ of $q_0$ with homogeneous flow-box coordinates $(t,z):\Omega \to (-2\varepsilon,2\varepsilon) \times Z$, where $Z$ is a conic transversal obtained from $\Sigma$, $H_{p_m}t=1$, $H_{p_m}z=0$ on $\Omega$, and the bicharacteristic segment is represented as $\gamma(t)=(t,z_0)$ for a fixed $z_0\in Z$.

Throughout, $\operatorname{WF}'(T)$ denotes the operator wavefront set of a properly supported pseudodifferential operator $T$, and all microlocal Sobolev statements are relative to properly supported order-zero elliptic cutoffs.

Assume further that the following local positive commutator package holds on $\Omega$. For every sufficiently small $\delta_0\in(0,\varepsilon/4)$ there are real scalar symbols $a\in S^{s-(m-1)/2}(\Omega)$, $b,e\in S^s(\Omega)$, and $r\in S^{2s-1}(\Omega)$, and properly supported quantizations $A\in\Psi^{s-(m-1)/2}(X)$, $B,E\in\Psi^s(X)$, and $R\in\Psi^{2s-1}(X)$ with principal symbols $a,b,e,r$, respectively, such that $\operatorname{WF}'(A)\Subset\Omega$, $B$ is elliptic on a conic neighbourhood of $\operatorname{WF}'(A)$ and in particular at $q_0$, $\operatorname{WF}'(E)$ is contained in the region $-\varepsilon<t<-\delta_0$, and, for the commutator sign convention used below, $H_{p_m}(a^2)=b^2-e^2+r$ modulo symbols whose operator wavefront set is disjoint from $\Omega$. This package includes the standard subprincipal absorption for the skew-adjoint part of $P$: all order-$2s$ terms contributed by $P-P^*$ in the localized commutator are already included in the displayed decomposition and are bounded by an arbitrarily small multiple of $B^*B$ plus an order-$2s-1$ localized remainder.

Assume also that the same package provides a regularized estimate as follows. Let $\Lambda_\tau\in\Psi^0(X)$, $0<\tau\leq1$, be any properly supported elliptic regularizing family with symbol $(1+\tau\lambda)^{-N}$ on $\Omega$, where $\lambda$ is a positive elliptic order-one symbol and $N$ is large. Set $A_\tau=\Lambda_\tau A$, $B_\tau=\Lambda_\tau B$, and $E_\tau=\Lambda_\tau E$. The regularized commutator has the form

\begin{align*} i(P^*A_\tau^*A_\tau-A_\tau^*A_\tau P)=B_\tau^*B_\tau-E_\tau^*E_\tau+R_\tau+F_\tau, \end{align*}

where $R_\tau$ is uniformly bounded in $\Psi^{2s-1}(X)$ with operator wavefront set contained in the controlled conic region and $F_\tau$ is uniformly smoothing after insertion of any microlocal cutoff supported in $\Omega$. For every distribution $v$ microlocally controlled in the upstream region and every $M>0$ with $v\in H^{-M}_{\mathrm{loc}}(X)$, these remainders satisfy

\begin{align*} |(R_\tau v,v)_{L^2(X)}|+|(F_\tau v,v)_{L^2(X)}|\leq C_1+C_2\|v\|_{H^{-M}_{\mathrm{loc}}(X)}^2+\eta\|B_\tau v\|_{L^2(X)}^2, \end{align*}

for constants independent of $\tau$, with $\eta>0$ chosen as small as needed. Finally, the package includes the uniform microlocal domination estimate

\begin{align*} \|A_\tau v\|_{H^{(m-1)/2}_{\mathrm{loc}}(X)}\leq C\|B_\tau v\|_{L^2(X)}+C\|v\|_{H^{-M}_{\mathrm{loc}}(X)}, \end{align*}

for all $0<\tau\leq1$ and all distributions $v$ microlocally supported in the commutant region, with $C$ independent of $\tau$.

Let $u \in \mathcal{D}'(X)$. Suppose that there is a conic neighbourhood $V \subset T^*X\setminus 0$ of $\gamma([-\varepsilon,\varepsilon])$ such that $Pu$ is microlocally in $H^{s-m+1}$ on $V$. Suppose also that for every sufficiently small $\delta>0$, $u$ is microlocally in $H^s$ on a conic neighbourhood of $\gamma([-\varepsilon,-\delta])$. Then, after replacing $\varepsilon>0$ by a smaller positive number if necessary, $u$ is microlocally in $H^s$ at $q_0$. Equivalently, $q_0 \notin \operatorname{WF}^s(u)$.