[proofplan] The proof is the standard positive-commutator propagation argument. First one reduces to a small homogeneous flow box near a characteristic covector and uses the real elliptic multiple $p_0=qp$ to parametrize the characteristic hypersurface by the Hamilton flow. In that flow box, a commutant is chosen so that its Hamilton derivative has a favorable sign: it is elliptic at the target point and controlled by an already-regular incoming region plus the microlocal regularity of $Pu$. The local estimate propagates $H^s$ regularity from the incoming slice to the target slice, after removing the lower-order error by induction on Sobolev order. Iterating the local statement along overlapping flow boxes, and then repeating the same argument for the reversed flow, proves that membership in $\operatorname{WF}^s(u)$ is constant along each maximal bicharacteristic segment where the hypotheses hold. [/proofplan]

[step:Reduce the assertion to propagation of regularity along one bicharacteristic] Let $\Sigma:=U\cap \operatorname{Char}(P)$. Since $q$ is elliptic on $U$, the equality $p_0=qp$ implies that $p$ and $p_0$ have the same zero set in $U$, so \begin{align*} \Sigma = \{\rho\in U:p(\rho)=0\} = \{\rho\in U:p_0(\rho)=0\} \end{align*} Because $p_0$ is real-valued and $d p_0\ne 0$ on $\Sigma$, $\Sigma$ is a smooth conic hypersurface in $U$, and the Hamilton vector field $H_{p_0}$ is tangent to $\Sigma$. Fix a maximally extended integral curve $\gamma:I\to \Sigma$ of $H_{p_0}$. It is enough to prove the following local propagation statement: if $t_0,t_1\in I$ lie in a compact subinterval $J\subset I$ and $u$ is microlocally in $H^s$ at $\gamma(t_0)$, then $u$ is microlocally in $H^s$ at $\gamma(t_1)$. Indeed, once the local statement is available in both flow directions, regularity at one point propagates to every other point in any compact subinterval of $I$. Hence if $\gamma(I)\setminus \operatorname{WF}^s(u)$ is nonempty, then all of $\gamma(I)$ is outside $\operatorname{WF}^s(u)$; otherwise every point of $\gamma(I)$ lies in $\operatorname{WF}^s(u)$. [/step]

[step:Place the characteristic set in homogeneous flow-box coordinates] Fix $\rho_0=\gamma(t_0)\in \Sigma$. Since $d p_0(\rho_0)\ne 0$ and $H_{p_0}$ is nonzero along the characteristic hypersurface in a sufficiently small conic neighborhood of $\rho_0$, the homogeneous flow-box theorem gives a conic neighborhood $V\subset U$ of $\rho_0$ and homogeneous coordinates $(r,\sigma,y):V\cap \Sigma \to (0,\infty)\times (-\epsilon,\epsilon)\times W$, where $r$ is the fiber-radial variable, $\sigma$ is a real flow parameter, and $W$ is an [open set](/page/Open%20Set) of transverse variables, such that on $V\cap\Sigma$ the Hamilton vector field has the form $H_{p_0}=\partial_\sigma$. After shrinking $V$, the portion of $\gamma$ in $V$ is represented by fixed transverse variables and varying $\sigma$. The microlocal elliptic multiple $L=QP$ has the same characteristic set as $P$ in $U$, because the principal symbol of $Q$ is elliptic there and the principal symbol of $L$ is $p_0=qp$. We do not apply $Q$ to $u$ in order to compare wave front sets; the point of introducing $L$ is only to replace $P$ by an order-zero operator with real principal symbol. Since $Q$ has order $-m$, the pseudodifferential mapping property gives that the hypothesis $Pu\in H^{s-m+1}$ microlocally on $U$ implies $Lu=QPu\in H^{s+1}$ microlocally on $U$. [/step]

[step:Choose a commutant whose Hamilton derivative is elliptic at the target]Choose two flow parameters $\sigma_-<\sigma_+$ in the coordinate interval, with $\gamma(\sigma_-)$ in an incoming region where $u$ is already microlocally in $H^s$ and $\gamma(\sigma_+)$ the target point. Choose a non-negative homogeneous symbol \begin{align*} b:T^*X\setminus 0\to [0,\infty) \end{align*} of order $s$ supported in $V$ whose restriction to $\Sigma$ is elliptic at $\gamma(\sigma_+)$. Choose another homogeneous symbol \begin{align*} g:T^*X\setminus 0\to [0,\infty) \end{align*} of order $s$ supported in the incoming region where $u$ is already microlocally in $H^s$. By the homogeneous escape-function construction in the flow box, shrinking $V$ if necessary, there is a real homogeneous symbol \begin{align*} a:T^*X\setminus 0\to \mathbb{R} \end{align*} of order $s+1/2$, supported in $V$, such that on $\Sigma$ \begin{align*} H_{p_0}(a^2)=b^2-g^2. \end{align*} Here the order is correct because $p_0$ has order $0$, so $H_{p_0}$ lowers symbolic order by $1$ and $H_{p_0}(a^2)$ has order $2s$. Extend $a$ smoothly off $\Sigma$ inside $V$ and take \begin{align*} A\in \Psi^{s+1/2}(X) \end{align*} to be a properly supported pseudodifferential operator with principal symbol $a$. The identity above is the precise substitute for the informal statement that the commutant is increasing along the flow. It gives a positive elliptic square $b^2$ at the target, while the negative square $g^2$ is supported only where the incoming $H^s$ regularity is already known.[/step]

[guided]The commutant must do more than have a symbol that is positive at the target. The commutator controls the Hamilton derivative $H_{p_0}(a^2)$, so the positive term must be elliptic where we want to prove regularity. This is why we prescribe the derivative of $a^2$, rather than merely choosing $a$ to be nonzero near the target. Choose a homogeneous symbol \begin{align*} b:T^*X\setminus 0\to [0,\infty) \end{align*} of order $s$ supported in the flow box and elliptic at the target covector $\gamma(\sigma_+)$. Choose a second homogeneous symbol \begin{align*} g:T^*X\setminus 0\to [0,\infty) \end{align*} of order $s$ supported in the incoming part of the same flow box, where $u$ is already known to be microlocally in $H^s$. In the coordinates on $\Sigma$, the Hamilton vector field is $H_{p_0}=\partial_\sigma$. Therefore the equation \begin{align*} H_{p_0}(a^2)=b^2-g^2 \end{align*} is solved along each bicharacteristic by integrating the right-hand side in the $\sigma$ variable, with $g$ chosen to cancel the accumulated contribution before the incoming edge of the flow box. This is the standard homogeneous escape-function construction: after shrinking the flow box and inserting transverse cutoffs, it produces a real homogeneous symbol \begin{align*} a:T^*X\setminus 0\to \mathbb{R} \end{align*} of order $s+1/2$, supported in $V$, satisfying the displayed identity on $\Sigma$. The order $s+1/2$ is forced by the normalization. Since $L=QP$ has order $0$, the Hamilton vector field of its principal symbol $p_0$ lowers symbolic order by $1$. Thus $a^2$ has order $2s+1$, and $H_{p_0}(a^2)$ has order $2s$, the same order as $b^2$ and $g^2$. Quantizing $a$ gives a properly supported operator \begin{align*} A\in \Psi^{s+1/2}(X). \end{align*} The term $b^2$ is elliptic at the target and hence will control an $H^s$ microlocal cutoff there. The term $g^2$ is the controlled error localized to the incoming region.[/guided]

[step:Apply the local positive commutator estimate to the normalized order-zero operator] We apply the local positive commutator estimate for scalar order-zero real-principal-type pseudodifferential operators to $L:=QP\in\Psi^0(X)$, microlocally on $U$. The estimate says: if an order-zero scalar operator has real principal symbol $\ell$, if $d\ell\ne 0$ on its characteristic set in a flow box, and if symbols $a,b,g$ of orders $s+1/2,s,s$ satisfy $H_\ell(a^2)=b^2-g^2$ on the characteristic set with $b$ elliptic at the target and $g$ supported in the incoming region, then properly supported quantizations give an estimate \begin{align*} \|Bu\|_{H^s} \le C\bigl(\|G u\|_{H^s}+\|E Lu\|_{H^{s+1}}+\|F u\|_{H^{s-\delta}}\bigr) \end{align*} for some $\delta>0$. Here $B,G,E,F\in\Psi^0(X)$ are properly supported microlocal cutoffs, $B$ is elliptic on the elliptic set of $b$, $G$ is microsupported where $g$ is supported, $E$ and $F$ are microsupported in $V$, and $C>0$ depends on finitely many symbol seminorms of $L$ and on the chosen cutoffs. The hypotheses of this estimate hold for $L$. Its principal symbol on $U$ is the real-valued function $p_0$, and $d p_0\ne 0$ on $\Sigma$, so $L$ is of real principal type in the flow box. The previous step constructed symbols $a,b,g$ with \begin{align*} H_{p_0}(a^2)=b^2-g^2 \end{align*} on $\Sigma$, with $b$ elliptic at the target and $g$ supported in the incoming region. The principal commutator calculation is therefore applied to $L$, not to $P$: since $L$ has order $0$ and $A\in\Psi^{s+1/2}(X)$, the commutator has order $2s$, and its principal symbol is governed by $H_{p_0}(a^2)$, up to the sign convention used in the estimate. The hypotheses give $\|E Lu\|_{H^{s+1}}<\infty$, because $Lu=QPu$ and $Q\in\Psi^{-m}(X)$ maps microlocal $H^{s-m+1}$ regularity to microlocal $H^{s+1}$ regularity. The incoming assumption gives $\|G u\|_{H^s}<\infty$. Therefore the estimate implies $\|Bu\|_{H^s}<\infty$ once the lower-order term $\|F u\|_{H^{s-\delta}}$ is known to be finite. The external result being used here is precisely the local positive commutator estimate for scalar order-zero real-principal-type pseudodifferential operators, in the form stated in the first paragraph of this step. [/step]

[step:Remove the lower-order term by induction on Sobolev order] For every distribution $u\in\mathcal{D}'(X)$ and every compactly supported microlocal cutoff $F$, there exists $N>0$ such that $F u\in H^{-N}(X)$. Choose $N$ so large that $s-k\delta\le -N$ for some integer $k\ge 0$. The local estimate applied first at the order $s-k\delta+\delta$, then at $s-k\delta+2\delta$, and so on up to $s$, propagates regularity one increment at a time. At every intermediate order $r\le s$, the forcing term is finite because $Lu\in H^{s+1}$ microlocally implies $Lu\in H^{r+1}$ microlocally, and the incoming $H^s$ regularity implies incoming $H^r$ regularity. At the initial level the lower-order term is finite by the distributional Sobolev bound. At each subsequent level the lower-order term has already been obtained at the previous level. Thus the lower-order term in the estimate at order $s$ is finite. Consequently $Bu\in H^s(X)$. Since $B$ is elliptic at the target point, this is precisely microlocal $H^s$ regularity of $u$ at the target point. [/step]

[step:Iterate the local propagation estimate along compact bicharacteristic segments] Let $K\subset I$ be a compact interval. The image $\gamma(K)$ is compact in $\Sigma$, so it is covered by finitely many homogeneous flow boxes of the kind constructed above. Starting from any point of $\gamma(K)$ where $u$ is microlocally in $H^s$, the local propagation result carries $H^s$ regularity to the next overlapping box in the direction of increasing flow parameter. Repeating this finitely many times propagates $H^s$ regularity to every later point of $\gamma(K)$. To propagate in the opposite direction, apply the same argument to the operator $-L$. This operator is still properly supported and order zero, satisfies $(-L)u=-Lu\in H^{s+1}$ microlocally on $U$, and has real principal symbol $-p_0$. The characteristic set is unchanged, the Hamilton vector field becomes $H_{-p_0}=-H_{p_0}$, and the real-principal-type hypotheses remain valid. Applying the local estimate to $-L$ propagates $H^s$ regularity toward decreasing flow parameter. [/step]

[step:Conclude invariance of the Sobolev wave front set along maximal segments] The preceding step shows that, on every compact subinterval of $I$, microlocal $H^s$ regularity at one point of the bicharacteristic implies microlocal $H^s$ regularity at every other point of that compact subinterval. Since any two points of the connected interval $I$ lie in some compact subinterval of $I$, microlocal $H^s$ regularity is constant along $\gamma(I)$. Therefore $\gamma(I)\cap \operatorname{WF}^s(u)$ is either empty or all of $\gamma(I)$. Since $\gamma$ was an arbitrary maximally extended integral curve of $H_{p_0}$ in $U\cap\operatorname{Char}(P)$, the set \begin{align*} \operatorname{WF}^s(u)\cap U\cap \operatorname{Char}(P) \end{align*} is a union of maximally extended null bicharacteristic segments of $H_{p_0}$ contained in $U\cap\operatorname{Char}(P)$. The maximality is relative to the interval on which the curve remains in the conic region where the real-principal-type hypothesis and the assumed microlocal regularity of $Pu$ hold. [/step]