[proofplan] We work in homogeneous symplectic coordinates near $q_0$ in which the Hamilton vector field is the derivative in the bicharacteristic parameter. In those coordinates we build a commutant of order $s-(m-1)/2$ whose Hamilton derivative produces an elliptic square of order $s$ at $q_0$, up to an error supported strictly on the already regular negative-time side. Quantizing this symbol and applying the positive commutator identity gives an estimate for a microlocal $H^s$ norm of $u$ near $q_0$. The term involving $Pu$ is controlled by the assumed microlocal $H^{s-m+1}$ regularity, and all upstream and lower-order terms are controlled either by the negative-time hypothesis or by regularization and absorption. [/proofplan]

[step:Straighten the bicharacteristic flow near $q_0$] By the homogeneous flow-box theorem for the nonvanishing Hamilton vector field $H_{p_m}$, after replacing $\varepsilon$ by a smaller positive number there is a conic neighbourhood $\Omega \subset T^*X\setminus 0$ of $q_0$, a number $\varepsilon_0 \in (0,\varepsilon]$, a conic transversal $Z$, and homogeneous coordinates \begin{align*} (t,z):\Omega \to (-2\varepsilon_0,2\varepsilon_0)\times Z \end{align*} such that $t$ is the Hamilton flow parameter, \begin{align*} H_{p_m}t=1 \end{align*} and $z$ is constant along the bicharacteristic flow on $\Omega$. Let $z_0\in Z$ denote the transversal coordinate of $q_0$. In these coordinates the bicharacteristic segment through $q_0$ is represented by \begin{align*} \gamma(t)=(t,z_0). \end{align*} We shrink $\Omega$ so that $\Omega \subset V$, where $V$ is the conic neighbourhood on which $Pu$ is microlocally in $H^{s-m+1}$. Choose $\delta_0 \in (0,\varepsilon_0/4)$. By the upstream hypothesis, after shrinking $\Omega$ in the transverse variables if necessary, $u$ is microlocally in $H^s$ on a conic neighbourhood of the part of $\Omega$ where \begin{align*} -\varepsilon_0 < t < -\delta_0. \end{align*} This is the only interpretation of the half-open negative segment used below: all error terms placed away from $t=0$ are supported in such a strictly negative-time region. [/step]

[step:Build a commutant that is elliptic at the target and monotone along the flow]We use the standard local positive commutator construction with the value of $\delta_0$ fixed in the previous step. It gives real scalar symbols \begin{align*} a\in S^{s-(m-1)/2}(\Omega),\quad b,e\in S^s(\Omega),\quad r\in S^{2s-1}(\Omega) \end{align*} where $B$ is elliptic on a conic neighbourhood of $\operatorname{WF}'(A)$, hence in particular $b$ is elliptic at $q_0$, and $e$ is supported in the strictly negative-time region where $u$ is already microlocally in $H^s$. With the commutator sign convention used below, these symbols satisfy \begin{align*} H_{p_m}(a^2)=b^2-e^2+r \end{align*} modulo symbols whose operator wavefront set is disjoint from the chosen conic neighbourhood of the bicharacteristic segment. The symbol $a$ has order \begin{align*} s-(m-1)/2, \end{align*} so the commutator with the order-$m$ operator produces a square of order $2s$. The statement's subprincipal absorption hypothesis also says that the order-$2s$ skew-adjoint contribution of $P-P^*$ is controlled by an arbitrarily small multiple of $b^2$ plus an order-$2s-1$ remainder on $\Omega$.[/step]

[guided]The purpose of this step is to isolate exactly what the local positive commutator construction must provide. We need a commutant symbol $a$ whose commutator with $P$ produces a positive order-$2s$ square at $q_0$, while every uncontrolled term is either one order lower or supported where the negative-time hypothesis already gives $H^s$ regularity of $u$. This is supplied by the standard positive commutator construction. For the chosen $\delta_0$, it gives symbols \begin{align*} a\in S^{s-(m-1)/2}(\Omega),\quad b,e\in S^s(\Omega),\quad r\in S^{2s-1}(\Omega) \end{align*} with $B$ elliptic on a conic neighbourhood of $\operatorname{WF}'(A)$, hence with $b$ elliptic at $q_0$, and with $e$ supported in the region $-\varepsilon_0<t<-\delta_0$, where $u$ is already microlocally in $H^s$. The exponent in the order of $a$ is chosen because a commutator with an order-$m$ operator raises $a^2$ by $m-1$, giving total order \begin{align*} 2\left(s-(m-1)/2\right)+m-1=2s. \end{align*} Thus the positive square has the correct order to detect microlocal $H^s$ regularity. With the sign convention used in the next step, the symbolic identity is \begin{align*} H_{p_m}(a^2)=b^2-e^2+r \end{align*} modulo symbols whose operator wavefront set is disjoint from the chosen tube. This statement includes the sign, support separation, and order reduction that are needed later: $b^2$ is the good elliptic square at $q_0$, $e^2$ is placed in the known upstream region, and $r$ has order $2s-1$. The same package also controls the order-$2s$ skew-adjoint subprincipal terms from $P-P^*$ by a small multiple of the good square plus an order-$2s-1$ remainder. This is the precise microlocal input used by the rest of the proof.[/guided]

[step:Quantize the symbols and regularize the commutator identity] Let \begin{align*} A\in\Psi^{s-(m-1)/2}(X),\qquad B\in\Psi^s(X),\qquad E\in\Psi^s(X),\qquad R\in\Psi^{2s-1}(X) \end{align*} be the properly supported quantizations supplied by the local positive commutator package, with principal symbols $a,b,e,r$, respectively. Let \begin{align*} \Lambda_\tau\in\Psi^0(X),\qquad 0<\tau\leq1, \end{align*} be a properly supported elliptic regularizing family whose full symbol is equal to $(1+\tau\lambda)^{-N}$ on the relevant conic set, with $N>0$ chosen so large that all pairings below are between $L^2$ functions. Define \begin{align*} A_\tau=\Lambda_\tau A. \end{align*} Then $A_\tau$ has order $s-(m-1)/2-N$ for fixed $\tau>0$ and $A_\tau\to A$ in the symbol topology of every slightly higher order as $\tau\downarrow0$. By the regularized commutator identity from the local positive commutator construction, the operator \begin{align*} i(P^*A_\tau^*A_\tau-A_\tau^*A_\tau P) \end{align*} has principal symbol equal, modulo the regularizing factor and wavefront-disjoint smoothing errors, to $H_{p_m}(a^2)$. Using the symbolic identity from the previous step and the sign convention fixed in the statement, we may write \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*} Here $B_\tau=\Lambda_\tau B$ and $E_\tau=\Lambda_\tau E$. The family $R_\tau$ is uniformly bounded in $\Psi^{2s-1}(X)$ with operator wavefront set contained in the controlled conic region specified by the commutator package. The family $F_\tau$ collects the symbolic errors whose operator wavefront set is disjoint from the chosen conic neighbourhood of the bicharacteristic segment; after inserting any properly supported microlocal cutoff supported in $\Omega$, it is uniformly smoothing and therefore has uniformly bounded pairings with the fixed distribution $u$. Choose an auxiliary properly supported microlocal cutoff $K\in\Psi^0(X)$ that is elliptic and equal to $1$ microlocally on a closed conic neighbourhood of the operator wavefront sets of $A,B,E,R_\tau$, with $\operatorname{WF}'(I-K)$ disjoint from the commutant region and with $\operatorname{WF}'(K)$ contained in $\Omega$. The wavefront-disjoint hypothesis on $F_\tau$ means that $F_\tau K$ and $K^*F_\tau K$ are uniformly smoothing families. Thus all pairings involving $F_\tau$ are taken after this proper microlocal insertion, and the terms involving $(I-K)u$ are tested only away from the commutant region. [/step]

[step:Estimate the commutator pairing by the regularity of $Pu$] For fixed $\tau>0$, the regularization makes the following identity legitimate. Put \begin{align*} Q_\tau=A_\tau^*A_\tau. \end{align*} Since the $L^2(X)$ inner product is linear in the first argument, \begin{align*} \bigl(i(P^*Q_\tau-Q_\tau P)u,u\bigr)_{L^2(X)}=2\operatorname{Im}\bigl(A_\tau Pu,A_\tau u\bigr)_{L^2(X)}. \end{align*} The order-$2s$ terms coming from the skew-adjoint part of $P$ and the commutators created by the regularizing family are not added again at this stage; by the formalized commutator package they are already included in the decomposition into $B_\tau^*B_\tau-E_\tau^*E_\tau+R_\tau+F_\tau$, with the absorbable part placed into the small multiple of $B_\tau^*B_\tau$ and the remaining lower-order part placed into $R_\tau+F_\tau$. Let \begin{align*} G\in\Psi^{s-m+1}(X) \end{align*} be a properly supported microlocal cutoff that is elliptic on the operator wavefront set of $A$. Let \begin{align*} G^{-1}\in\Psi^{-s+m-1}(X) \end{align*} denote a microlocal parametrix for $G$ on that conic set. Thus there are properly supported smoothing operators $S_1,S_2\in\Psi^{-\infty}(X)$ microlocally near $\operatorname{WF}'(A)$ such that $G^{-1}G=I+S_1$ and $GG^{-1}=I+S_2$ there. Since $Pu$ is microlocally in $H^{s-m+1}$ on $V$ and the operator wavefront set of $A$ is contained in $V$, we have $GPu\in L^2(X)$. Microlocally on $\operatorname{WF}'(A)$ we may write \begin{align*} A_\tau Pu=A_\tau G^{-1}GPu+A_\tau S_1Pu+S_{\tau}u, \end{align*} where $S_{\tau}\in\Psi^{-\infty}(X)$ is uniformly smoothing after insertion of a cutoff supported in $\Omega$. The term $A_\tau S_1Pu+S_\tau u$ is therefore bounded by a fixed local negative Sobolev norm of $u$, after choosing $M>0$ so large that $u\in H^{-M}_{\mathrm{loc}}(X)$. The composition $A_\tau G^{-1}$ has order \begin{align*} s-(m-1)/2-s+m-1=(m-1)/2. \end{align*} Thus $A_\tau Pu$ is paired in $H^{-(m-1)/2}$ against $A_\tau u$ in $H^{(m-1)/2}$, rather than by an $L^2$-boundedness assertion for $A_\tau G^{-1}$. Since the formalized commutator package requires $B$ to be elliptic on a conic neighbourhood of $\operatorname{WF}'(A)$, we choose the support of $G$ inside that elliptic neighbourhood. The uniform microlocal domination estimate included in the package gives \begin{align*} \|A_\tau u\|_{H^{(m-1)/2}_{\mathrm{loc}}(X)}\leq C\|B_\tau u\|_{L^2(X)}+C\|u\|_{H^{-M}_{\mathrm{loc}}(X)}, \end{align*} with $C$ independent of $\tau$. Also $GPu\in L^2(X)$, and the operator $A_\tau G^{-1}$ has order $(m-1)/2$, so $A_\tau Pu$ is bounded in $H^{-(m-1)/2}_{\mathrm{loc}}(X)$ by $\|GPu\|_{L^2(X)}$ plus a fixed local negative Sobolev norm of $u$. Sobolev duality between $H^{-(m-1)/2}_{\mathrm{loc}}(X)$ and $H^{(m-1)/2}_{\mathrm{loc}}(X)$, followed by the Cauchy-Schwarz inequality and the Young inequality $2xy\leq \eta x^2+\eta^{-1}y^2$, gives, for every fixed $\eta>0$, \begin{align*} 2|\operatorname{Im}(A_\tau Pu,A_\tau u)_{L^2(X)}|\leq \eta\|B_\tau u\|_{L^2(X)}^2+C_{\eta,0}\|GPu\|_{L^2(X)}^2+C_{\eta,1}\|u\|_{H^{-M}_{\mathrm{loc}}(X)}^2. \end{align*} Here $M>0$ is fixed large enough that the distribution $u$ belongs locally to $H^{-M}$, the constants $C_{\eta,0},C_{\eta,1}>0$ depend on $\eta$, the chosen microlocal cutoffs, the parametrix $G^{-1}$, and finitely many uniform seminorms of $A_\tau G^{-1}$, but are independent of $\tau$. This estimate is the point where the hypothesis on $Pu$ is used. The Sobolev order $s-m+1$ is exactly the order that pairs with the order $s$ positive square produced by the commutator of an order-$m$ operator. [/step]

[step:Control the upstream and lower-order terms]Taking the $L^2$ pairing of the symbolic commutator identity with $u$ gives \begin{align*} \|B_\tau u\|_{L^2(X)}^2\leq \|E_\tau u\|_{L^2(X)}^2+|\bigl(R_\tau u,u\bigr)_{L^2(X)}|+|\bigl(F_\tau u,u\bigr)_{L^2(X)}|+|\bigl(i(P^*A_\tau^*A_\tau-A_\tau^*A_\tau P)u,u\bigr)_{L^2(X)}|. \end{align*} The operator $E$ is supported in the negative-time conic region where $u$ is microlocally in $H^s$. Since $E$ has order $s$, an elliptic order-$s$ cutoff supported in that region sends $u$ to $L^2(X)$, and the regularizing factor $\Lambda_\tau$ is uniformly bounded on $L^2(X)$ microlocally there. Hence $\|E_\tau u\|_{L^2(X)}$ is bounded uniformly in $\tau$. The family $R_\tau$ has order $2s-1$, one order lower than $B_\tau^*B_\tau$, which has order $2s$. The standard lower-order regularized remainder estimate applies because the operator wavefront sets of the remainders are contained in the union of the region where $B$ is elliptic, the strictly upstream region where $u$ is already microlocally $H^s$, and the wavefront-disjoint smoothing region. Therefore, after shrinking the tube and adding a compactly supported elliptic cutoff in a slightly larger conic neighbourhood, there are constants $C_{R,0},C_{R,1}>0$ independent of $\tau$ such that \begin{align*} |\bigl(R_\tau u,u\bigr)_{L^2(X)}|+|\bigl(F_\tau u,u\bigr)_{L^2(X)}|\leq C_{R,0}+C_{R,1}\|u\|_{H^{-M}_{\mathrm{loc}}(X)}^2+\frac{1}{4}\|B_\tau u\|_{L^2(X)}^2. \end{align*} The constants $C_{R,0}$ and $C_{R,1}$ come from the assumed regularized remainder estimate, the fixed enlargement cutoff, and finitely many seminorms of the uniformly bounded families $R_\tau$ and $F_\tau$; in particular, they are independent of $\tau$. Combining this with the estimate for the $Pu$ term and choosing $\eta>0$ small enough yields \begin{align*} \|B_\tau u\|_{L^2(X)}^2\leq C_{B}\left(1+\|GPu\|_{L^2(X)}^2+\|u\|_{H^{-M}_{\mathrm{loc}}(X)}^2\right) \end{align*} for a constant $C_B>0$ independent of $\tau$.[/step]

[guided]We now turn the symbolic sign into an actual estimate. The commutator identity says that the good square $B_\tau^*B_\tau$ is bounded by three kinds of terms: the upstream square $E_\tau^*E_\tau$, lower-order symbolic remainders, and the pairing involving $Pu$. The upstream square is controlled because $E$ was deliberately supported where the hypothesis already gives microlocal $H^s$ regularity of $u$. In other words, an elliptic order-$s$ cutoff in that negative-time region sends $u$ to $L^2(X)$, and every regularized operator $E_\tau$ has wavefront set inside that same known region. Hence \begin{align*} \|E_\tau u\|_{L^2(X)} \end{align*} is bounded independently of $\tau$. The lower-order term $R_\tau$ has order $2s-1$, while $B_\tau^*B_\tau$ has order $2s$. The regularized remainder estimate applies to the present distribution $u$ for the following reason: the previous step placed $u$ in $H^s$ microlocally on the strictly upstream region containing $\operatorname{WF}'(E)$, the commutator construction places the remaining controlled part of $\operatorname{WF}'(R_\tau)$ inside the conic region where $B$ is elliptic on $\operatorname{WF}'(A)$, and the term $F_\tau$ is uniformly smoothing after insertion of a cutoff supported in $\Omega$. Since every distribution is locally in $H^{-M}$ for some sufficiently large $M>0$, all hypotheses of the standard remainder estimate are satisfied by $v=u$. Hence, with constants independent of $\tau$, we obtain \begin{align*} |\bigl(R_\tau u,u\bigr)_{L^2(X)}|+|\bigl(F_\tau u,u\bigr)_{L^2(X)}|\leq C_{R,0}+C_{R,1}\|u\|_{H^{-M}_{\mathrm{loc}}(X)}^2+\frac{1}{4}\|B_\tau u\|_{L^2(X)}^2. \end{align*} The constants $C_{R,0}$ and $C_{R,1}$ are fixed by the assumed remainder estimate and the chosen microlocal cutoffs; they do not depend on $\tau$. The term involving $Pu$ is controlled by the assumption that $Pu$ is microlocally in $H^{s-m+1}$ on the whole tube. Applying Cauchy-Schwarz with the Young inequality $2xy\leq \eta x^2+\eta^{-1}y^2$ gives \begin{align*} 2|\operatorname{Im}(A_\tau Pu,A_\tau u)_{L^2(X)}|\leq \eta\|B_\tau u\|_{L^2(X)}^2+C_{\eta,0}\|GPu\|_{L^2(X)}^2+C_{\eta,1}\|u\|_{H^{-M}_{\mathrm{loc}}(X)}^2. \end{align*} The constants $C_{\eta,0}$ and $C_{\eta,1}$ depend on $\eta$, the fixed parametrix, and the fixed microlocal cutoffs, but not on $\tau$. Choosing $\eta>0$ small enough allows the $\eta\|B_\tau u\|_{L^2(X)}^2$ term and the $\frac14\|B_\tau u\|_{L^2(X)}^2$ term to be moved to the left-hand side. This gives a uniform bound \begin{align*} \|B_\tau u\|_{L^2(X)}^2\leq C_B\left(1+\|GPu\|_{L^2(X)}^2+\|u\|_{H^{-M}_{\mathrm{loc}}(X)}^2\right), \end{align*} with $C_B$ independent of the regularization parameter $\tau$.[/guided]

[step:Remove the regularization and conclude microlocal $H^s$ regularity at $q_0$]The uniform estimate for $\|B_\tau u\|_{L^2(X)}$ implies, by weak compactness in $L^2_{\mathrm{loc}}(X)$, that along a sequence $\tau_j\downarrow0$ the distributions $B_{\tau_j}u$ converge weakly in $L^2_{\mathrm{loc}}(X)$ to some $w\in L^2_{\mathrm{loc}}(X)$. We now identify this weak limit. Let $\phi\in C_c^\infty(X)$. Since $B_{\tau_j}^*\phi=B^*\Lambda_{\tau_j}^*\phi$ and $\Lambda_{\tau_j}^*\phi\to\phi$ in $C^\infty$ on compact sets, continuity of $B^*$ on test functions gives \begin{align*} B_{\tau_j}^*\phi\to B^*\phi \end{align*} in $C^\infty$ on compact sets. Therefore distributional continuity of $u$ gives \begin{align*} (B_{\tau_j}u)(\phi)=u(B_{\tau_j}^*\phi)\to u(B^*\phi)=(Bu)(\phi). \end{align*} Thus $B_{\tau_j}u\to Bu$ in $\mathcal{D}'(X)$. The weak $L^2_{\mathrm{loc}}(X)$ limit has the same distributional limit, so $w=Bu$ as distributions, and hence \begin{align*} Bu\in L^2_{\mathrm{loc}}(X). \end{align*} Since $B$ is elliptic at $q_0$ of order $s$, the standard elliptic microlocal regularity theorem for pseudodifferential operators implies that $u$ is microlocally in $H^s$ near $q_0$. Therefore $q_0\notin\operatorname{WF}^s(u)$. Equivalently, there exists an operator \begin{align*} Q\in\Psi^0(X) \end{align*} elliptic at $q_0$ such that \begin{align*} Qu\in H^s_{\mathrm{loc}}(X). \end{align*} This is precisely microlocal $H^s$ regularity of $u$ at $q_0$, completing the proof.[/step]

[guided]The uniform estimate is independent of the regularization parameter, so it gives compactness rather than merely a bound for each fixed regularized operator. Choose a sequence $\tau_j\downarrow0$. Since the sequence $B_{\tau_j}u$ is bounded in $L^2_{\mathrm{loc}}(X)$, weak compactness gives a subsequence, still denoted $B_{\tau_j}u$, converging weakly in $L^2_{\mathrm{loc}}(X)$ to some function $w\in L^2_{\mathrm{loc}}(X)$. We must identify $w$ with the distribution $Bu$. Let $\phi\in C_c^\infty(X)$ be a test function. The adjoints satisfy $B_{\tau_j}^*\phi=B^*\Lambda_{\tau_j}^*\phi$. Since $\Lambda_{\tau_j}^*\phi\to\phi$ in $C^\infty$ on compact subsets and pseudodifferential operators act continuously on test functions, we have \begin{align*} B_{\tau_j}^*\phi\to B^*\phi \end{align*} in $C^\infty$ on compact subsets. By continuity of the distribution $u$ on test functions, \begin{align*} (B_{\tau_j}u)(\phi)=u(B_{\tau_j}^*\phi)\to u(B^*\phi)=(Bu)(\phi). \end{align*} Thus $B_{\tau_j}u\to Bu$ in $\mathcal{D}'(X)$. The same sequence also converges weakly in $L^2_{\mathrm{loc}}(X)$ to $w$, and weak $L^2_{\mathrm{loc}}(X)$ convergence implies distributional convergence to $w$. Distributional limits are unique, so $w=Bu$ as distributions. Hence \begin{align*} Bu\in L^2_{\mathrm{loc}}(X). \end{align*} Now we use ellipticity. The operator $B\in\Psi^s(X)$ is elliptic at $q_0$, so elliptic microlocal regularity gives an order-zero operator $Q\in\Psi^0(X)$ elliptic at $q_0$ such that \begin{align*} Qu\in H^s_{\mathrm{loc}}(X). \end{align*} This is exactly the definition of microlocal $H^s$ regularity at $q_0$. Therefore $q_0\notin\operatorname{WF}^s(u)$, completing the proof.[/guided]