[proofplan] We prove first the forward statement, from $a$ to $b$. For a fixed Sobolev order $s$, local Sobolev propagation for real-principal-type operators moves microlocal $H^s$ regularity a short positive time along the Hamilton flow, provided $Pu$ has the required shifted Sobolev regularity nearby. Since $\gamma([a,b])$ is compact and disjoint from $WF(Pu)$, that source regularity is available uniformly on a finite ordered chain of local flow boxes covering the segment. Iterating the local propagation step gives microlocal $H^s$ regularity at every point of the segment; since $s$ is arbitrary, this is microlocal smoothness. The backward statement follows by applying the same local theorem to the reversed Hamilton direction. [/proofplan]

[step:Translate microlocal smoothness into arbitrary Sobolev regularity] Fix $s \in \mathbb{R}$. Let $H^s_{\mathrm{mic}}(u)$ denote the subset of $T^*X \setminus 0$ at which $u$ is microlocally in $H^s$. Thus $q \in H^s_{\mathrm{mic}}(u)$ means that there exists an [elliptic operator](/page/Elliptic%20Operator) $A \in \Psi_{\mathrm{cl}}^0(X)$ at $q$ such that $Au \in H^s_{\mathrm{loc}}(X)$. Similarly, $q \in H^r_{\mathrm{mic}}(Pu)$ means that $Pu$ is microlocally in $H^r$ at $q$. The assumption $\gamma([a,b]) \cap WF(Pu)=\varnothing$ means that for every $r \in \mathbb{R}$ and every $t \in [a,b]$, the point $\gamma(t)$ belongs to $H^r_{\mathrm{mic}}(Pu)$. In particular, for the fixed order $s$, every point of $\gamma([a,b])$ belongs to $H^{s-m+1}_{\mathrm{mic}}(Pu)$. The assumption $\gamma(a) \notin WF(u)$ means that $\gamma(a) \in H^s_{\mathrm{mic}}(u)$ for every $s \in \mathbb{R}$, and hence for the fixed $s$ chosen above. [/step]

[step:Choose local flow boxes where Sobolev propagation applies]We use the local Sobolev propagation theorem for real-principal-type operators, in the following form: if $q_0 \in \operatorname{Char}(P)$, $Pu$ is microlocally in $H^{s-m+1}$ near the bicharacteristic through $q_0$, and $u$ is microlocally in $H^s$ on an incoming part of that bicharacteristic, then $u$ is microlocally in $H^s$ on a sufficiently short outgoing part of the same bicharacteristic. This is the local propagation of singularities input for the proof. Since the theorem could not be resolved to a database theorem ID here, we record it as a prerequisite: (citing a result not yet in the wiki: local Sobolev propagation of singularities for real-principal-type operators). For each $t_0 \in [a,b]$, apply this local theorem at $q_0=\gamma(t_0)$. Because $P$ is of real principal type, the Hamilton vector field $H_p$ is nonzero on the characteristic set in the relevant conic direction, so the bicharacteristic admits a local flow-box description near $\gamma(t_0)$. Therefore there exist an open interval $I_{t_0} \subset \mathbb{R}$ containing $t_0$ and a conic neighbourhood $V_{t_0} \subset T^*X \setminus 0$ of $\gamma(t_0)$ such that the following implication holds inside $V_{t_0}$: microlocal $H^s$ regularity of $u$ at one sufficiently incoming point of $\gamma(I_{t_0})$, together with microlocal $H^{s-m+1}$ regularity of $Pu$ on $V_{t_0}$, implies microlocal $H^s$ regularity of $u$ at all later points of a smaller subinterval of $I_{t_0}$. The family $\{I_{t_0}\}_{t_0 \in [a,b]}$ is an open cover of the compact interval $[a,b]$. Choose a finite subcover and refine it, if necessary, to a finite ordered chain of intervals \begin{align*} J_0, J_1, \dots, J_N \subset [a,b] \end{align*} with corresponding conic neighbourhoods \begin{align*} V_0, V_1, \dots, V_N \subset T^*X \setminus 0 \end{align*} such that $a \in J_0$, $b \in J_N$, the intervals cover $[a,b]$, and $J_j \cap J_{j+1}$ contains a nonempty interval for each $j \in \{0,\dots,N-1\}$. The ordering is chosen so that increasing $j$ follows increasing parameter $t$ along the bicharacteristic.[/step]

[guided]The local theorem only propagates regularity through a short piece of the Hamilton flow, so we must turn the compact interval $[a,b]$ into finitely many short pieces. For every $t_0 \in [a,b]$, the point $\gamma(t_0)$ lies in $\operatorname{Char}(P)$, and the real-principal-type hypothesis says that the Hamilton flow is nondegenerate there in the characteristic direction. This is exactly the geometric hypothesis needed for the local propagation theorem. For the fixed Sobolev order $s$, the local theorem requires source regularity of $Pu$ at order $s-m+1$. We have already verified that this holds at every point of $\gamma([a,b])$, because $\gamma([a,b])$ is disjoint from $WF(Pu)$. Thus each point $\gamma(t_0)$ has a conic neighbourhood $V_{t_0}$ and a parameter interval $I_{t_0}$ on which the local propagation implication is valid. Now compactness is used only to avoid infinitely many propagation steps. Since $[a,b]$ is compact and the intervals $I_{t_0}$ cover it, finitely many of them cover $[a,b]$. By shrinking and ordering these intervals along the parameter $t$, we obtain intervals $J_0,\dots,J_N$ with overlaps $J_j \cap J_{j+1}$ of positive length. The overlaps are essential: they are the places where the regularity obtained from one local propagation step becomes the incoming regularity needed to start the next step.[/guided]

[step:Iterate the local propagation theorem along the ordered chain] We prove by induction on $j \in \{0,\dots,N\}$ that $u$ is microlocally in $H^s$ at every point of $\gamma(J_j)$ already reached from the left endpoint $a$. For $j=0$, the point $\gamma(a)$ is microlocally in $H^s$ by hypothesis. On $V_0$, the distribution $Pu$ is microlocally in $H^{s-m+1}$ by the disjointness of $\gamma([a,b])$ from $WF(Pu)$. Applying the local Sobolev propagation theorem in the forward Hamilton direction gives microlocal $H^s$ regularity of $u$ throughout $\gamma(J_0)$ after shrinking $J_0$ within the chosen flow box if needed. Assume that the assertion holds through $J_j$ for some $j < N$. Since $J_j \cap J_{j+1}$ contains a nonempty interval, choose a parameter \begin{align*} \tau_j \in J_j \cap J_{j+1}. \end{align*} By the induction hypothesis, $u$ is microlocally in $H^s$ at $\gamma(\tau_j)$. On $V_{j+1}$, the source term $Pu$ is microlocally in $H^{s-m+1}$, again because $WF(Pu)$ is disjoint from the whole compact strip. Applying the local propagation theorem in the forward Hamilton direction from the incoming point $\gamma(\tau_j)$ propagates microlocal $H^s$ regularity across $\gamma(J_{j+1})$. This proves the induction step. Therefore $u$ is microlocally in $H^s$ at every point of \begin{align*} \gamma([a,b]) = \bigcup_{j=0}^{N} \gamma(J_j). \end{align*} [/step]

[step:Pass from fixed Sobolev order to absence of wave front set] The Sobolev order $s \in \mathbb{R}$ was arbitrary. Hence for every $s \in \mathbb{R}$ and every $t \in [a,b]$, the point $\gamma(t)$ belongs to $H^s_{\mathrm{mic}}(u)$. By the Sobolev characterization of the smooth wave front set, a point $q \in T^*X \setminus 0$ is absent from $WF(u)$ exactly when $u$ is microlocally in $H^s$ at $q$ for every $s \in \mathbb{R}$. Applying this characterization at each $q=\gamma(t)$ gives \begin{align*} \gamma([a,b]) \cap WF(u) = \varnothing. \end{align*} This proves the forward propagation statement. [/step]

[step:Reverse the Hamilton direction to prove the endpoint-interchanged statement] Assume instead that $\gamma(b) \notin WF(u)$. Define the reversed bicharacteristic segment \begin{align*} \tilde{\gamma}: [a,b] &\to \operatorname{Char}(P) \end{align*} \begin{align*} t &\mapsto \gamma(a+b-t). \end{align*} This curve is the same compact characteristic segment with the opposite orientation. The hypothesis on the source term is unchanged, since \begin{align*} \tilde{\gamma}([a,b]) = \gamma([a,b]) \end{align*} and this set is disjoint from $WF(Pu)$. The initial point of the reversed segment is $\tilde{\gamma}(a)=\gamma(b)$, which is microlocally smooth by assumption. Applying the forward argument to the reversed Hamilton direction, equivalently using the local commutator propagation estimate with the opposite sign, gives \begin{align*} \tilde{\gamma}([a,b]) \cap WF(u) = \varnothing. \end{align*} Since $\tilde{\gamma}([a,b])=\gamma([a,b])$, this is exactly \begin{align*} \gamma([a,b]) \cap WF(u) = \varnothing. \end{align*} The endpoint-interchanged statement follows. [/step]