Let $X$ be a smooth manifold, let $m,s \in \mathbb{R}$, and let $P:C_c^\infty(X)\to C^\infty(X)$ be a properly supported scalar pseudodifferential operator in $\Psi^m(X)$, extended by duality to a continuous map $\mathcal{D}'(X)\to \mathcal{D}'(X)$. Let $p$ denote the homogeneous scalar principal symbol of $P$ on $T^*X\setminus 0$, and let $U\subset T^*X\setminus 0$ be a conic [open set](/page/Open%20Set) on which $P$ is of real principal type.

Assume that there exists an elliptic symbol $q\in S^{-m}(U)$ such that $p_0:=qp$ is real-valued on $U$ and

\begin{align*} d p_0(\rho)\ne 0 \end{align*}

for every $\rho\in U\cap \operatorname{Char}(P)$, where

\begin{align*} \operatorname{Char}(P)\cap U=\{\rho\in U:p(\rho)=0\}=\{\rho\in U:p_0(\rho)=0\}. \end{align*}

Assume also that $q$ is quantized microlocally on $U$ by a properly supported [elliptic operator](/page/Elliptic%20Operator) $Q\in \Psi^{-m}(X)$ whose principal symbol on $U$ is $q$, and set $L:=QP\in \Psi^0(X)$ microlocally on $U$. Thus $L$ has real scalar principal symbol $p_0$ on $U$. Let $H_{p_0}$ be the Hamilton vector field of $p_0$ on $U$. If $u\in \mathcal{D}'(X)$ and $Pu$ is microlocally in $H^{s-m+1}$ at every point of $U$, then $Lu=QPu$ is microlocally in $H^{s+1}$ at every point of $U$, and for every maximally extended integral curve

\begin{align*} \gamma:I\to U\cap \operatorname{Char}(P) \end{align*}

of $H_{p_0}$, with $I\subset\mathbb{R}$ an interval, the set

\begin{align*} \gamma(I)\cap \operatorname{WF}^s(u) \end{align*}

is either empty or all of $\gamma(I)$. Equivalently, $\operatorname{WF}^s(u)\cap U\cap \operatorname{Char}(P)$ is a union of maximally extended null bicharacteristic segments of $H_{p_0}$ contained in $U\cap \operatorname{Char}(P)$.