[proofplan] We first remove all non-characteristic covectors by microlocal elliptic regularity, so the only possible propagation occurs inside $\operatorname{Char}(P)$. The main local input is the standard positive-commutator Sobolev propagation theorem: if $Pu$ is microlocally $H^{s-m+1}$ near a short bicharacteristic segment and $u$ is microlocally $H^s$ on the incoming part, then $u$ is microlocally $H^s$ slightly farther along the Hamilton flow. Iterating the local step along compact subintervals and then varying $s$ gives propagation of the $C^\infty$ wavefront set along maximal null bicharacteristics. [/proofplan]

[step:Reduce possible singularities to the characteristic set]Let $p: T^*X \setminus 0 \to \mathbb{R}$ denote the real homogeneous principal symbol of $P$, and let \begin{align*} \operatorname{Ell}(P) := \{(x,\xi) \in T^*X \setminus 0 : p(x,\xi) \neq 0\} \end{align*} denote the elliptic set of $P$. [Microlocal elliptic regularity for pseudodifferential operators](/theorems/8163) states that, for every properly supported scalar classical operator $P \in \Psi^m_{\mathrm{cl}}(X)$ and every $u \in \mathcal{D}'(X)$, \begin{align*} WF(u) \cap \operatorname{Ell}(P) \subset WF(Pu). \end{align*} The external result used here is the microlocal elliptic parametrix theorem: if the principal symbol of $P$ is nonzero at $\rho$ and $Pu$ is microlocally smooth at $\rho$, then $u$ is microlocally smooth at $\rho$. Its hypotheses match because $P$ is properly supported and scalar classical, and ellipticity at $\rho$ is exactly the condition $p(\rho) \neq 0$. Therefore \begin{align*} WF(u) \setminus WF(Pu) \subset \operatorname{Char}(P). \end{align*} It remains to prove that this set is invariant under the Hamilton flow of $p$ inside $\operatorname{Char}(P) \setminus WF(Pu)$.[/step]

[guided]The first point is that propagation can only happen where the operator is characteristic. Define the elliptic set of $P$ by \begin{align*} \operatorname{Ell}(P) := \{(x,\xi) \in T^*X \setminus 0 : p(x,\xi) \neq 0\}. \end{align*} On this set the principal symbol is invertible in the scalar sense, so microlocal elliptic regularity applies: if $Pu$ is smooth microlocally at a covector where $P$ is elliptic, then $u$ is smooth microlocally there. In wavefront notation this says \begin{align*} WF(u) \cap \operatorname{Ell}(P) \subset WF(Pu). \end{align*} This is the precise mechanism that removes non-characteristic directions from the problem. Now let $\rho \in WF(u) \setminus WF(Pu)$. Since $\rho \notin WF(Pu)$, elliptic regularity prevents $\rho$ from lying in $\operatorname{Ell}(P)$. Hence $p(\rho) = 0$, so $\rho \in \operatorname{Char}(P)$. Therefore \begin{align*} WF(u) \setminus WF(Pu) \subset \operatorname{Char}(P). \end{align*} Thus the only remaining issue is not whether singularities live on the characteristic set, but how they are arranged along the Hamilton flow on that characteristic set.[/guided]

[step:Prove the local Sobolev propagation estimate along a short bicharacteristic segment]For $s \in \mathbb{R}$, let $WF^s(u) \subset T^*X \setminus 0$ denote the Sobolev wavefront set of $u$, so that $\rho \notin WF^s(u)$ means that some properly supported $Q \in \Psi^0_{\mathrm{cl}}(X)$ elliptic at $\rho$ satisfies $Qu \in H^s_{\mathrm{loc}}(X)$. If $A \subset T^*X \setminus 0$, the phrase "$u$ is microlocally in $H^s$ on $A$" means $A \cap WF^s(u) = \varnothing$; equivalently, every point of $A$ has a conic neighbourhood on which this exclusion holds. [claim:Local Sobolev propagation across a known regular incoming segment] Let $s \in \mathbb{R}$, let $a<c<b$, let $\gamma: [a,b] \to \operatorname{Char}(P)$ be an integral curve of $H_p$, and let $K := \gamma([a,b])$. Assume $K$ is contained in an open conic coordinate neighbourhood $V \subset T^*X \setminus 0$, meaning that $V$ is invariant under positive fiber scaling and is equipped with smooth local coordinates on $T^*X \setminus 0$. Assume there is a real-valued coordinate function $\tau: V \to \mathbb{R}$ satisfying $H_p\tau > 0$ on $V \cap \operatorname{Char}(P)$. Assume that $Pu$ is microlocally in $H^{s-m+1}$ on an open conic neighbourhood of $K$, and assume that \begin{align*} \gamma([a,c]) \cap WF^s(u) = \varnothing. \end{align*} Then, after possibly shrinking $V$ and $b-c>0$ while keeping $[a,c]$ fixed, one has \begin{align*} \gamma([a,b]) \cap WF^s(u) = \varnothing. \end{align*} The same assertion with the interval direction reversed holds after replacing $P$ by $-P$. [/claim] [proof] This is the standard local positive-commutator propagation theorem for scalar classical pseudodifferential operators of real principal type, stated in the non-vacuous boundary-crossing form. The external result used is: if $P$ is properly supported scalar classical with real principal symbol $p$, $H_p$ is nonzero on the characteristic set, $Pu$ is microlocally in $H^{s-m+1}$ near a compact short characteristic segment, and $u$ is microlocally in $H^s$ on an incoming one-sided neighbourhood of the left part of that segment, then $u$ is microlocally in $H^s$ on a slightly longer forward segment. The length of the added forward segment is obtained after fixing the coordinate patch, the incoming neighbourhood, and the commutator cutoffs; it is therefore a neighbourhood-size conclusion at the boundary of the known regular set, not a pointwise existence statement depending on an arbitrary starting point. The hypotheses match the present situation. The operator $P$ is properly supported and scalar classical, $p$ is real, and the real-principal-type assumption gives $H_p \neq 0$ on $\operatorname{Char}(P)$. The open conic coordinate neighbourhood $V$ supplies the local coordinates needed for the symbol construction, while the coordinate function $\tau$ orients the segment by $H_p\tau > 0$. The assumption $\gamma([a,c]) \cap WF^s(u)=\varnothing$ gives the incoming $H^s$ regularity required by the theorem on an open conic neighbourhood of $\gamma([a,c])$ after shrinking, because $WF^s(u)$ is closed conic and $\gamma([a,c])$ is compact. The assumption on $Pu$ is exactly the required microlocal $H^{s-m+1}$ regularity near the full short segment. Applying the positive-commutator theorem gives a number $b>c$, after shrinking the original right endpoint if necessary, for which $\gamma([a,b]) \cap WF^s(u)=\varnothing$. For the reverse-direction assertion, $-P$ has principal symbol $-p$, the same characteristic set, and Hamilton vector field $H_{-p}=-H_p$, so forward propagation for $-P$ is backward propagation for $P$. [/proof][/step]

[guided]The purpose of this step is not to reprove the full positive-commutator theorem, but to apply it in the precise form needed for continuation. Fix $s \in \mathbb{R}$ and a short segment $\gamma([a,b])$ of an integral curve of $H_p$ inside $\operatorname{Char}(P)$. The Sobolev wavefront set $WF^s(u)$ is defined so that $\rho \notin WF^s(u)$ precisely when there exists a properly supported order-zero pseudodifferential operator $Q \in \Psi^0_{\mathrm{cl}}(X)$ elliptic at $\rho$ such that $Qu \in H^s_{\mathrm{loc}}(X)$. The subtle point is the incoming side. A positive-commutator propagation theorem does not say that regularity at a single endpoint automatically propagates by a uniformly controlled distance. Its useful local form says this: if $u$ is already microlocally in $H^s$ on an incoming segment $\gamma([a,c])$, if $Pu$ is microlocally in $H^{s-m+1}$ near a slightly longer segment, and if the Hamilton flow is oriented by a coordinate $\tau$ with $H_p\tau>0$, then $u$ is microlocally in $H^s$ across the boundary point $\gamma(c)$ and on a short forward segment $\gamma([c,b])$ after shrinking $b-c>0$. We verify the hypotheses. The operator $P$ is properly supported and scalar classical by the theorem statement. Its principal symbol $p: T^*X \setminus 0 \to \mathbb{R}$ is real and homogeneous, and the real-principal-type assumption gives $H_p(\rho) \neq 0$ for every $\rho \in \operatorname{Char}(P)$. After shortening the segment, nonvanishing of $H_p$ gives an open conic coordinate neighbourhood $V \subset T^*X \setminus 0$ of $\gamma([a,b])$ and a real coordinate function $\tau: V \to \mathbb{R}$ with $H_p\tau > 0$ on $V \cap \operatorname{Char}(P)$. Here "open conic" means invariant under positive fiber scaling, and "coordinate function" means one of the smooth local coordinates on that neighbourhood. The inequality $H_p\tau > 0$ fixes which side is incoming and which side is forward. The regularity hypotheses are also exactly those available in applications. The condition $\gamma([a,c]) \cap WF^s(u)=\varnothing$, together with compactness of $\gamma([a,c])$ and closedness of $WF^s(u)$, gives an open conic neighbourhood of the incoming segment on which $u$ is microlocally in $H^s$. The condition on $Pu$ is $\gamma([a,b]) \cap WF^{s-m+1}(Pu)=\varnothing$ after shrinking to an open conic neighbourhood of the full short segment. The standard local positive-commutator propagation theorem for real principal type operators therefore applies and gives, after choosing commutator cutoffs supported inside $V$, a shortened endpoint $b>c$ such that \begin{align*} \gamma([a,b]) \cap WF^s(u)=\varnothing. \end{align*} This is the non-vacuous assertion needed later: regularity crosses the boundary of a known regular interval, rather than merely restating regularity at points already known to be regular.[/guided]

[step:Iterate the local estimate by an open and closed continuation argument]Let $\gamma: I \to \operatorname{Char}(P) \setminus WF(Pu)$ be an integral curve of $H_p$, and let $J \subset I$ be a compact interval. Since $\gamma(J)$ is compact and disjoint from the closed conic set $WF(Pu)$, the distribution $Pu$ is microlocally smooth at every point of $\gamma(J)$. Thus, for every $s \in \mathbb{R}$, $Pu$ is microlocally in $H^{s-m+1}$ on a conic neighbourhood of $\gamma(J)$ after shrinking finitely many conic neighbourhoods covering $\gamma(J)$. Fix $s \in \mathbb{R}$ and suppose $\gamma(t_0) \notin WF^s(u)$ for some $t_0 \in J$. Define \begin{align*} R_s := \{t \in J : \gamma(t) \notin WF^s(u)\}. \end{align*} The set $R_s$ is open in $J$, because $WF^s(u)$ is closed conic and $\gamma$ is continuous. Let $C_s$ be the connected component of $R_s$ containing $t_0$. If the right endpoint of $C_s$ were an interior point $b$ of $J$, choose $a,c \in C_s$ with $a<c<b$ and with $c$ sufficiently close to $b$ that the compact segment from $a$ to a point just to the right of $b$ lies in one of the conic coordinate neighbourhoods used in the local propagation claim. Because $C_s$ is a connected component of the [open set](/page/Open%20Set) $R_s$, we have $\gamma([a,c]) \cap WF^s(u)=\varnothing$. Because $Pu$ is microlocally in $H^{s-m+1}$ near $\gamma(J)$, the local Sobolev propagation claim applies across the boundary point $c$ and gives regularity on $\gamma([a,b'])$ for some $b'>c$. Choosing $c$ close enough to $b$ within the fixed local coordinate neighbourhood makes $b'>b$, so $\gamma(b) \notin WF^s(u)$ and regularity holds slightly beyond $b$. This contradicts maximality of the component $C_s$. Applying the reverse-direction form of the claim, equivalently applying the forward claim to $-P$ whose Hamilton field is $-H_p$, rules out an interior left endpoint in the same way. Therefore $C_s$ has no interior endpoint in $J$. Since $J$ is connected and $C_s$ is a nonempty relatively open interval in $J$, this forces $C_s=J$. Hence, for every $s \in \mathbb{R}$, \begin{align*} \gamma(t_0) \notin WF^s(u) \quad \Longrightarrow \quad \gamma(t) \notin WF^s(u) \text{ for all } t \in J. \end{align*}[/step]

[guided]The iteration needs a continuation argument, not just the phrase "repeat the local estimate." Fix a Sobolev order $s \in \mathbb{R}$ and assume $\gamma(t_0) \notin WF^s(u)$ at one point of the compact interval $J$. We record the times where this same Sobolev regularity is known by defining \begin{align*} R_s := \{t \in J : \gamma(t) \notin WF^s(u)\}. \end{align*} This set is open in $J$: if $\gamma(t) \notin WF^s(u)$, then closedness of $WF^s(u)$ gives a conic neighbourhood of $\gamma(t)$ avoiding $WF^s(u)$, and continuity of $\gamma$ pulls that neighbourhood back to an open interval of times. Let $C_s$ be the connected component of $R_s$ containing $t_0$. We show that this component cannot stop at an interior point of $J$. Suppose, for instance, that $b$ is the right endpoint of $C_s$ and $b$ lies in the interior of $J$. Choose $a,c \in C_s$ with $a<c<b$ and with $c$ close to $b$. We choose them so that the segment from $a$ to a point just to the right of $b$ lies in one conic coordinate neighbourhood for the local propagation theorem. This is possible because $H_p$ is nonzero on the characteristic set and $b$ is an interior time of $J$. The compactness of $\gamma(J)$ and the assumption $\gamma(J) \cap WF(Pu)=\varnothing$ ensure that, for this fixed $s$, $Pu$ is microlocally in $H^{s-m+1}$ near that short segment. Since $[a,c] \subset C_s$, we have \begin{align*} \gamma([a,c]) \cap WF^s(u)=\varnothing. \end{align*} The local Sobolev propagation claim applies to this incoming regular segment and propagates regularity across $\gamma(c)$ to a short interval on its right. Because the claim is a neighbourhood statement after the coordinate patch and cutoffs are fixed, taking $c$ sufficiently close to $b$ makes the propagated interval pass through $b$ and slightly beyond it. This puts $b$ in $R_s$ and extends regularity past $b$, contradicting the choice of $b$ as the endpoint of the component. The same reasoning rules out a left endpoint. To move left, apply the already verified local theorem to $-P$. Its principal symbol is $-p$, its characteristic set is the same as that of $P$, and its Hamilton vector field is $H_{-p}=-H_p$, so forward propagation for $-P$ is backward propagation for $P$. Thus $C_s$ has no interior endpoint in the connected compact interval $J$. Since $C_s$ is nonempty and relatively open in $J$, it follows that $C_s=J$. Consequently \begin{align*} \gamma(t_0) \notin WF^s(u) \quad \Longrightarrow \quad \gamma(t) \notin WF^s(u) \text{ for all } t \in J. \end{align*}[/guided]

[step:Pass from Sobolev propagation to smooth wavefront propagation]Recall that, with the convention that $WF^s(u)$ records failure of microlocal $H^s$ regularity, the smooth wavefront set is the union of the Sobolev wavefront sets: \begin{align*} WF(u) = \bigcup_{s \in \mathbb{R}} WF^s(u). \end{align*} Equivalently, $\rho \notin WF(u)$ means $\rho \notin WF^s(u)$ for every $s \in \mathbb{R}$. Let $\gamma: I \to \operatorname{Char}(P) \setminus WF(Pu)$ be a null bicharacteristic and suppose $\gamma(t_0) \notin WF(u)$ for some $t_0 \in I$. Then for every $s \in \mathbb{R}$, \begin{align*} \gamma(t_0) \notin WF^s(u). \end{align*} By Sobolev propagation along each compact interval $J \subset I$ containing $t_0$, we have \begin{align*} \gamma(t) \notin WF^s(u) \end{align*} for every $t \in J$ and every $s \in \mathbb{R}$. Therefore $\gamma(t) \notin WF(u)$ for every $t \in J$. Since $J \subset I$ was arbitrary, $\gamma(t) \notin WF(u)$ for every $t \in I$.[/step]

[guided]The passage from Sobolev wavefront sets to the smooth wavefront set uses the correct set-theoretic direction. Since $WF^s(u)$ is the set of points where microlocal $H^s$ regularity fails, smooth microlocal regularity fails exactly when some Sobolev order fails. Thus \begin{align*} WF(u) = \bigcup_{s \in \mathbb{R}} WF^s(u). \end{align*} Taking complements gives the form we need: $\rho \notin WF(u)$ if and only if $\rho \notin WF^s(u)$ for every $s \in \mathbb{R}$. Now assume $\gamma(t_0) \notin WF(u)$. By the complement formulation, every Sobolev order is regular at $\gamma(t_0)$: \begin{align*} \gamma(t_0) \notin WF^s(u) \end{align*} for every $s \in \mathbb{R}$. Fix a compact interval $J \subset I$ containing $t_0$. The iteration step applies separately to each $s$ and gives \begin{align*} \gamma(t) \notin WF^s(u) \end{align*} for every $t \in J$ and every $s \in \mathbb{R}$. Applying the same complement formulation again, $\gamma(t) \notin WF(u)$ for every $t \in J$. Since every point of $I$ lies in some compact subinterval $J \subset I$ containing $t_0$, this proves $\gamma(t) \notin WF(u)$ for all $t \in I$.[/guided]

[step:Identify the maximal connected bicharacteristic components]Define \begin{align*} S := WF(u) \setminus WF(Pu). \end{align*} The first step showed that $S \subset \operatorname{Char}(P) \setminus WF(Pu)$. The previous step showed that, along every null bicharacteristic contained in $\operatorname{Char}(P) \setminus WF(Pu)$, either all points of the connected bicharacteristic component lie outside $WF(u)$ or all points lie in $WF(u)$, relative to the maximal interval on which the curve remains in $\operatorname{Char}(P) \setminus WF(Pu)$. Therefore $S$ is saturated by the Hamilton flow of $p$ in $\operatorname{Char}(P) \setminus WF(Pu)$. Equivalently, $S$ is a union of maximally extended connected integral curves of $H_p$ in that open conic set. These integral curves are precisely the maximally extended null bicharacteristics of $P$ in $\operatorname{Char}(P) \setminus WF(Pu)$, which proves the theorem.[/step]

[guided]Let \begin{align*} S := WF(u) \setminus WF(Pu). \end{align*} The elliptic reduction already proved that every point of $S$ lies in $\operatorname{Char}(P) \setminus WF(Pu)$. Now take a maximal integral curve $\gamma: I \to \operatorname{Char}(P) \setminus WF(Pu)$ of $H_p$. The smooth propagation step says that if one point $\gamma(t_0)$ is outside $WF(u)$, then every point $\gamma(t)$ is outside $WF(u)$. Taking the contrapositive along the same connected curve, if one point of the curve lies in $WF(u)$, then no point of the curve can lie outside $WF(u)$. Thus each maximal connected integral curve in $\operatorname{Char}(P) \setminus WF(Pu)$ is either entirely contained in $S$ or entirely disjoint from $S$. This is exactly the statement that $S$ is saturated by the Hamilton flow. Since null bicharacteristics of $P$ are, by definition, the integral curves of $H_p$ inside $\operatorname{Char}(P)$, the saturated components are the maximally extended null bicharacteristics in $\operatorname{Char}(P) \setminus WF(Pu)$. Hence $WF(u) \setminus WF(Pu)$ is a union of such maximally extended null bicharacteristics.[/guided]