[proofplan] Strict hyperbolicity gives real simple characteristic roots, so locally the characteristic variety splits into smooth real sheets. On each sheet the additional hypothesis $dp_m \neq 0$ makes the principal symbol real principal type, and the Hamiltonian vector field is tangent to the characteristic sheet. The Duistermaat-Hörmander propagation theorem for real principal type operators then implies that $WF(u)$, away from $WF(Pu)$, propagates along the null bicharacteristics of $H_{p_m}$. Restricting those bicharacteristics to a connected component of $\Sigma \setminus WF(Pu)$ gives the asserted local invariance. [/proofplan]

[step:Identify the characteristic sheets as smooth hypersurfaces]Fix an open conic subset $\Gamma \subset T^*U \setminus 0$ as in the statement, and fix one smooth connected characteristic sheet $\Sigma \subset \operatorname{Char}(P) \cap \Gamma$. By hypothesis, $\Sigma$ is a smooth connected submanifold of $T^*U \setminus 0$ and \begin{align*} p_m|_{\Sigma}=0. \end{align*} Since $dp_m \neq 0$ at every point of $\Sigma$, the [implicit function theorem](/theorems/52) shows that $\operatorname{Char}(P)$ is a smooth hypersurface near every point of $\Sigma$. Thus the sheet structure needed for the propagation argument is supplied by the hypotheses on $\Gamma$: each chosen $\Sigma$ is a smooth connected component of the regular characteristic hypersurface $\operatorname{Char}(P) \cap \Gamma$. Strict hyperbolicity is the structural assumption ensuring that, in adapted coordinates away from the zero spatial covector regime, the characteristic roots are real and simple; the proof below uses the explicitly stated regular-sheet condition $dp_m \neq 0$ on $\Sigma$.[/step]

[guided]We first isolate the geometric object on which propagation will occur. The set $\operatorname{Char}(P)$ is the zero set of the real-valued smooth function $p_m: T^*U \setminus 0 \to \mathbb{R}$. On the chosen conic region $\Gamma$, the statement already assumes that this zero set decomposes into smooth connected characteristic sheets. We fix one such sheet $\Sigma$. The condition $dp_m \neq 0$ on $\Sigma$ is the regular-level-set condition for the equation $p_m=0$. Therefore, by the implicit function theorem, near every point of $\Sigma$ the characteristic set is a smooth hypersurface in $T^*U \setminus 0$. This regular hypersurface structure, rather than any auxiliary coordinate graph description, is the geometric input needed for propagation. Strict hyperbolicity explains why these hypersurfaces should be viewed as characteristic sheets: in adapted local coordinates, the principal symbol has real simple roots in the time covariable wherever the spatial covector is nonzero. However, the present argument does not require us to parametrize every point of $\Sigma$ by such a root graph. The theorem statement has already declared the relevant open conic region $\Gamma$ and the smooth sheets inside $\operatorname{Char}(P) \cap \Gamma$, and the proof will use precisely those declared sheets.[/guided]

[step:Recognize the localized operator as real principal type on the sheet]Let $\omega$ denote the canonical symplectic form on $T^*U \setminus 0$. The Hamiltonian vector field of $p_m$ is the smooth vector field \begin{align*} H_{p_m}: T^*U \setminus 0 \to T(T^*U \setminus 0) \end{align*} defined by \begin{align*} \omega(H_{p_m},V)=dp_m(V) \end{align*} for every tangent vector $V$ to $T^*U \setminus 0$. A null bicharacteristic arc of $p_m$ is a smooth integral curve $\gamma: I \to \operatorname{Char}(P)$, where $I \subset \mathbb{R}$ is an interval and $\gamma'(s)=H_{p_m}(\gamma(s))$ for every $s \in I$. Because $\omega$ is nondegenerate and $dp_m \neq 0$ on $\Sigma$, we have $H_{p_m} \neq 0$ at every point of $\Sigma$. Since $p_m$ is real-valued, homogeneous of degree $m$ in the cotangent variable, and has nonvanishing differential on $\Sigma$, the operator $P$ is of real principal type microlocally near $\Sigma$. Moreover, $H_{p_m}$ is tangent to $\Sigma$. Indeed, along the Hamiltonian flow the derivative of $p_m$ is \begin{align*} H_{p_m}p_m = dp_m(H_{p_m}) = \omega(H_{p_m},H_{p_m}) = 0, \end{align*} because $\omega$ is alternating. Hence integral curves of $H_{p_m}$ starting on $\Sigma$ remain in $\operatorname{Char}(P)$ for as long as they are defined, and locally remain on the same connected sheet $\Sigma$.[/step]

[guided]We now verify the real-principal-type hypotheses that will be needed for propagation. The canonical symplectic form $\omega$ on $T^*U \setminus 0$ is nondegenerate, and the Hamiltonian vector field $H_{p_m}$ is defined by the identity \begin{align*} \omega(H_{p_m},V)=dp_m(V) \end{align*} for every tangent vector $V$ to $T^*U \setminus 0$. Since $dp_m \neq 0$ at every point of $\Sigma$, nondegeneracy of $\omega$ implies that $H_{p_m}$ cannot vanish on $\Sigma$: if $H_{p_m}=0$ at a point, then $dp_m(V)=\omega(0,V)=0$ for every tangent vector $V$ at that point, contradicting $dp_m \neq 0$. This is exactly the microlocal real-principal-type condition for the scalar differential operator $P$ on the sheet. The principal symbol $p_m$ is real-valued by hypothesis, it is smooth on $T^*U \setminus 0$, and its differential does not vanish on the characteristic sheet $\Sigma$. Therefore the characteristic set is a regular hypersurface near $\Sigma$, and the associated Hamiltonian vector field is nonzero there. It remains to check that the Hamiltonian flow actually follows the characteristic sheet. Along an integral curve of $H_{p_m}$, the derivative of the defining function $p_m$ is $H_{p_m}p_m$. By the defining identity for $H_{p_m}$ and the alternating property of the symplectic form, \begin{align*} H_{p_m}p_m = dp_m(H_{p_m}) = \omega(H_{p_m},H_{p_m}) = 0. \end{align*} Thus $p_m$ is constant along the Hamiltonian flow. If an integral curve starts on $\Sigma \subset \operatorname{Char}(P)$, then initially $p_m=0$, so $p_m$ remains zero for as long as the curve is defined. Hence the curve remains in the characteristic set, and locally it stays on the same smooth connected sheet $\Sigma$.[/guided]

[step:Apply propagation of singularities on the real principal type sheet]We use the classical Duistermaat-Hörmander [propagation of singularities theorem for real principal type operators](/theorems/8164). Its relevant form is the following: if a scalar pseudodifferential or differential operator has real principal symbol $p$ and is of real principal type on a conic characteristic hypersurface, then for every distribution $v$, the set \begin{align*} WF(v) \setminus WF(Pv) \end{align*} inside that hypersurface is invariant along every null bicharacteristic segment of $H_p$ that stays in the characteristic hypersurface and avoids $WF(Pv)$. We apply this theorem with $v=u$ and $p=p_m$ after choosing a coordinate patch in $U$ and a microlocal cutoff supported in a sufficiently small open conic neighbourhood $\Gamma_0 \subset \Gamma$ of an arbitrary point of $\Sigma$. Since $P$ is a differential operator, this localization preserves the principal symbol $p_m$ on $\Gamma_0$ and places the operator in the standard properly supported local form required by the propagation theorem. The hypotheses are satisfied on $\Gamma_0$ because $p_m$ is real-valued, smooth on $T^*U \setminus 0$, and $dp_m \neq 0$ on $\Sigma \cap \Gamma_0$. Therefore, microlocally on $\Sigma \cap \Gamma_0$, \begin{align*} WF(u) \setminus WF(Pu) \end{align*} is invariant along integral curves of $H_{p_m}$ for every segment that remains in $\Sigma \cap \Gamma_0$ and does not meet $WF(Pu)$. Covering any compact subsegment of a bicharacteristic in $C$ by finitely many such conic neighbourhoods and iterating the local conclusion patches the microlocal statement along the whole subsegment.[/step]

[guided]This is the step where the microlocal propagation theorem is used. The theorem we need is the classical [Duistermaat-Hörmander propagation of singularities theorem](/theorems/8192) for real principal type operators. In the form used here, it says that if a scalar pseudodifferential or differential operator has real principal symbol $p$ and is of real principal type on a conic characteristic hypersurface, then for every distribution $v$ the set \begin{align*} WF(v) \setminus WF(Pv) \end{align*} is invariant along every null bicharacteristic segment of $H_p$ that remains in that characteristic hypersurface and avoids $WF(Pv)$. We must verify its hypotheses in the present conic region. Choose a coordinate patch in $U$ and a sufficiently small open conic neighbourhood $\Gamma_0 \subset \Gamma$ of an arbitrary point of $\Sigma$, then insert a microlocal cutoff supported in $\Gamma_0$. Because $P$ is a differential operator, this localization does not change the principal symbol on $\Gamma_0$ and gives the standard properly supported local representative used in the propagation theorem. First, the principal symbol $p_m$ is real-valued by assumption. Second, $p_m$ is smooth on $T^*U \setminus 0$ because $P$ has smooth coefficients. Third, on $\Sigma \cap \Gamma_0$, the differential $dp_m$ never vanishes. This is exactly the real-principal-type condition on the characteristic hypersurface: the characteristic equation $p_m=0$ defines a smooth hypersurface, and the Hamiltonian vector field is nonzero there. Since every compact subsegment of a bicharacteristic in $C$ is covered by finitely many such neighbourhoods, the local propagation conclusions can be iterated along the subsegment. The theorem then says that singularities of $u$ cannot start or stop along a null bicharacteristic segment while that segment stays inside the characteristic hypersurface and outside $WF(Pu)$. More precisely, inside $\Sigma \cap \Gamma_0$, \begin{align*} WF(u) \setminus WF(Pu) \end{align*} is invariant under the integral curves of $H_{p_m}$ for all such segments. We apply this with $v=u$ and $p=p_m$. Since $P$ has principal symbol $p_m$, the null bicharacteristics are exactly the integral curves of $H_{p_m}$ contained in the characteristic set. Lower-order terms of $P$ do not alter these curves: the propagation direction is determined by the principal symbol appearing in the principal commutator calculation. Hence, on the sheet $\Sigma$, the singular support in phase space propagates along the Hamiltonian flow of $p_m$ away from $WF(Pu)$.[/guided]

[step:Restrict the propagated bicharacteristics to the component avoiding $WF(Pu)$]Let $C$ be a connected component of $\Sigma \setminus WF(Pu)$, and define \begin{align*} S_C := (WF(u) \setminus WF(Pu)) \cap C. \end{align*} Let $\gamma: I \to \Sigma$ be an integral curve of $H_{p_m}$, where $I \subset \mathbb{R}$ is an interval, and suppose that $\gamma(I) \subset C$. By the propagation theorem applied in the preceding step, if $\gamma(t_0) \in S_C$ for some $t_0 \in I$, then $\gamma(t) \in WF(u) \setminus WF(Pu)$ for every $t \in I$. Since $\gamma(I) \subset C$, this gives $\gamma(t) \in S_C$ for every $t \in I$. Thus $S_C$ is invariant under the Hamiltonian flow of $p_m$ for as long as the flow remains in $C$. Equivalently, $S_C$ is a union of connected null bicharacteristic arcs of $H_{p_m}$ contained in $C$. This proves the claimed propagation on each characteristic sheet and each connected component of $\Sigma \setminus WF(Pu)$.[/step]

[guided]The propagation theorem gives a statement on the whole characteristic sheet, but the theorem we are proving asks for the statement on one connected component of the sheet after removing $WF(Pu)$. We therefore fix a connected component \begin{align*} C \subset \Sigma \setminus WF(Pu) \end{align*} and define \begin{align*} S_C := (WF(u) \setminus WF(Pu)) \cap C. \end{align*} Let $\gamma: I \to \Sigma$ be a null bicharacteristic arc of $p_m$, where $I \subset \mathbb{R}$ is an interval, and assume that $\gamma(I) \subset C$. This last condition is exactly the phrase "as long as the flow remains in $C$": the curve does not leave the chosen component and, because $C \cap WF(Pu)=\varnothing$, it does not meet the singular set of $Pu$. Suppose that $\gamma(t_0) \in S_C$ for some $t_0 \in I$. Since $\gamma(I)$ lies in the characteristic sheet and avoids $WF(Pu)$, the propagation result from the previous step applies to the whole segment $\gamma(I)$. It gives \begin{align*} \gamma(t) \in WF(u) \setminus WF(Pu) \end{align*} for every $t \in I$. Because $\gamma(I) \subset C$, this is the same as \begin{align*} \gamma(t) \in (WF(u) \setminus WF(Pu)) \cap C = S_C \end{align*} for every $t \in I$. Hence $S_C$ is invariant under the Hamiltonian flow of $p_m$ for every flow segment contained in $C$. Since null bicharacteristic arcs are precisely the integral-curve segments of $H_{p_m}$ in the characteristic set, this invariance is equivalent to saying that $S_C$ is a union of connected null bicharacteristic arcs contained in $C$.[/guided]