[proofplan] We pull the Hamilton vector field $H_{p_m}$ back from $\Lambda$ to the critical manifold $C_{\phi}\cap W$ and use the hypothesis $H_{p_m}t\ne 0$ to regard $C_0$ as a transverse Cauchy surface. The symbolic action of $P$ on $e^{i\phi}a$ produces a hierarchy of transport equations: the leading eikonal term vanishes because $p_m|_{\Lambda}=0$, and the first nonzero equation is a first-order linear equation along the lifted bicharacteristics. We solve this hierarchy recursively with the prescribed homogeneous initial data, extend the solutions off the critical set to homogeneous amplitudes supported in $W$, and use classical Borel summation. The resulting residual vanishes to infinite order on the parametrized Lagrangian patch, which is exactly the microlocal smoothing condition for $P I_{\phi}(a)$ along $\Lambda$. [/proofplan]

[step:Pull back the Hamilton flow to the critical set]Let \begin{align*} \kappa:C_{\phi}\cap W\to\Lambda \end{align*} be the diffeomorphism from the statement, defined by $\kappa(x,\theta)=(x,\partial_x\phi(x,\theta))$. Define the lifted Hamilton vector field \begin{align*} V\in\mathfrak{X}(C_{\phi}\cap W) \end{align*} by \begin{align*} d\kappa_{\rho}(V_{\rho})=H_{p_m,\kappa(\rho)} \end{align*} for every $\rho\in C_{\phi}\cap W$. This is well-defined and smooth because $\kappa$ is a diffeomorphism and $H_{p_m}$ is tangent to $\Lambda$. The real-principal-type hypothesis $dp_m\ne 0$ is one of the hypotheses ensuring that this Hamilton field gives the transport direction in the symbolic calculus used below. Let \begin{align*} \tau:C_{\phi}\cap W\to\mathbb{R} \end{align*} be the restriction of the coordinate function $t$ to $C_{\phi}\cap W$. Since $\kappa$ preserves the base point $x=(t,y)$, the condition $H_{p_m}t\ne 0$ on $\Lambda$ implies \begin{align*} V\tau\ne 0 \end{align*} on $C_{\phi}\cap W$. Therefore $C_0=\tau^{-1}(0)$ is a smooth hypersurface in $C_{\phi}\cap W$ transverse to $V$. By the assumed global flow-box property on the chosen conic patch, every point of $C_{\phi}\cap W$ lies on a unique integral curve of $V$ meeting $C_0$ exactly once. Equivalently, there are an open interval $I\subset\mathbb{R}$ containing $0$ and a conic diffeomorphism \begin{align*} F:I\times C_0\to C_{\phi}\cap W \end{align*} such that $F(0,\rho_0)=\rho_0$ and \begin{align*} \partial_s F(s,\rho_0)=V_{F(s,\rho_0)} \end{align*} for every $(s,\rho_0)\in I\times C_0$.[/step]

[guided]The phase parametrizes the Lagrangian by the map \begin{align*} \kappa:C_{\phi}\cap W\to\Lambda,\qquad \rho\mapsto (x,\partial_x\phi(\rho)). \end{align*} The statement assumes that this map is a diffeomorphism onto $\Lambda$. This lets us transfer every vector field on $\Lambda$ back to the critical set without ambiguity. In particular, for each point $\rho\in C_{\phi}\cap W$, there is a unique vector $V_{\rho}\in T_{\rho}(C_{\phi}\cap W)$ satisfying \begin{align*} d\kappa_{\rho}(V_{\rho})=H_{p_m,\kappa(\rho)}. \end{align*} This defines a smooth vector field $V$ because both $\kappa$ and $\kappa^{-1}$ are smooth. The transversality condition is the reason the initial data may be prescribed at $t=0$. Let \begin{align*} \tau:C_{\phi}\cap W\to\mathbb{R} \end{align*} be the function obtained by restricting the coordinate $t$ to the critical set. Since $\kappa$ keeps the base coordinate $x=(t,y)$ fixed, differentiating $t$ along $V$ on the critical set is the same as differentiating $t$ along $H_{p_m}$ on $\Lambda$. Hence the hypothesis $H_{p_m}t\ne 0$ gives \begin{align*} V\tau\ne 0. \end{align*} Thus $\tau^{-1}(0)=C_0$ is transverse to the flow lines of $V$. Finally, the theorem assumes more than local transversality: it assumes that every bicharacteristic in the selected patch meets the section $t=0$ exactly once. Pulling this statement back through $\kappa$, every integral curve of $V$ in $C_{\phi}\cap W$ meets $C_0$ exactly once. Therefore we may use flow coordinates \begin{align*} F:I\times C_0\to C_{\phi}\cap W \end{align*} with $F(0,\rho_0)=\rho_0$ and $\partial_sF=V\circ F$. These are precisely the coordinates in which first-order transport equations become ordinary differential equations in $s$.[/guided]

[step:Write the symbolic transport hierarchy on the critical set] We use the standard local symbolic calculus for applying the scalar differential operator $P$ to Lagrangian oscillatory integrals written with the real nondegenerate phase $\phi$ and the fixed coordinate half-density convention. For each classical amplitude $a\in S^r_{\mathrm{cl}}(U\times\Gamma)$, there is a classical amplitude \begin{align*} Q_{\phi}(a)\in S^{r+m}_{\mathrm{cl}}(U\times\Gamma) \end{align*} depending linearly on $a$, on $P$, and on finitely many derivatives of $\phi$, such that \begin{align*} P I_{\phi}(a)=I_{\phi}(Q_{\phi}(a)) \end{align*} microlocally on the conic patch under consideration. If \begin{align*} a\sim\sum_{j=0}^{\infty}a_{r-j}, \end{align*} then the homogeneous expansion of $Q_{\phi}(a)$ has terms \begin{align*} Q_{\phi}(a)\sim\sum_{j=0}^{\infty}q_{r+m-j}, \end{align*} where each $q_{r+m-j}$ is determined by $a_r,\dots,a_{r-j}$ and by the coefficients of $P$ and $\phi$. The leading term is \begin{align*} q_{r+m}=p_m(x,\partial_x\phi(x,\theta))a_r. \end{align*} On $C_{\phi}\cap W$, this term vanishes because $p_m|_{\Lambda}=0$ and $\kappa(C_{\phi}\cap W)=\Lambda$. The next coefficient, restricted to $C_{\phi}\cap W$, has the form \begin{align*} q_{r+m-1}|_{C_{\phi}\cap W}=\mathcal{T}_r(a_r|_{C_{\phi}\cap W}), \end{align*} where $\mu$ denotes an arbitrary real order parameter and, for each $\mu\in\mathbb{R}$, \begin{align*} \mathcal{T}_{\mu}:C^\infty(C_{\phi}\cap W)\to C^\infty(C_{\phi}\cap W) \end{align*} is the first-order linear transport operator of the form \begin{align*} \mathcal{T}_{\mu}c=Vc+\gamma_{\mu}c. \end{align*} The differential part is exactly the lifted Hamilton vector field $V$ by the standard transport formula for real principal type Lagrangian oscillatory integrals. Here \begin{align*} \gamma_{\mu}:C_{\phi}\cap W\to\mathbb{C} \end{align*} is a smooth homogeneous function of degree $m-1$ in the conic variable after the fixed coordinate half-density convention has been chosen. More generally, after $a_r,\dots,a_{r-j+1}$ have been chosen, the condition \begin{align*} q_{r+m-j}|_{C_{\phi}\cap W}=0 \end{align*} is equivalent to the inhomogeneous transport equation \begin{align*} \mathcal{T}_{r-j}(a_{r-j}|_{C_{\phi}\cap W})=f_{r-j} \end{align*} for a smooth homogeneous function \begin{align*} f_{r-j}:C_{\phi}\cap W\to\mathbb{C} \end{align*} of degree $r-j+m-1$, determined only by $a_r|_{C_{\phi}\cap W},\dots,a_{r-j+1}|_{C_{\phi}\cap W}$, by $P$, and by $\phi$. This is the transport hierarchy associated to the pair $(P,\phi)$ in the local symbolic calculus. The lower-order coefficient $\gamma_{\mu}$ depends on the chosen density and symbol normalization, but its precise formula is irrelevant for solvability because the differential part is the nonvanishing vector field $V$. [/step]

[step:Solve the first transport equation from the prescribed leading data] Let \begin{align*} c_r:C_{\phi}\cap W\to\mathbb{C} \end{align*} denote the unknown restriction $a_r|_{C_{\phi}\cap W}$. The leading transport equation is \begin{align*} \mathcal{T}_r c_r=0,\qquad c_r|_{C_0}=b_r. \end{align*} In the flow coordinates $F:I\times C_0\to C_{\phi}\cap W$, define the coefficient map \begin{align*} \Gamma_r:I\times C_0\to\mathbb{C} \end{align*} by $\Gamma_r(s,\rho_0)=\gamma_r(F(s,\rho_0))$. Here $\mathcal{L}^1$ denotes one-dimensional Lebesgue measure on the flow-parameter interval $I\subset\mathbb{R}$. For each $\rho_0\in C_0$, the function \begin{align*} u_r:I\to\mathbb{C},\qquad s\mapsto c_r(F(s,\rho_0)) \end{align*} must solve the linear ordinary differential equation \begin{align*} \frac{d u_r}{ds}(s)+\Gamma_r(s,\rho_0)u_r(s)=0,\qquad u_r(0)=b_r(\rho_0). \end{align*} Thus define \begin{align*} c_r(F(s,\rho_0)):=b_r(\rho_0)\exp\left(-\int_0^s\Gamma_r(\sigma,\rho_0)\,d\mathcal{L}^1(\sigma)\right). \end{align*} The smooth dependence theorem for ordinary differential equations gives $c_r\in C^\infty(C_{\phi}\cap W)$. Because $F$ is conic, $b_r$ is homogeneous of degree $r$, and the transport coefficients preserve the homogeneous grading, $c_r$ is homogeneous of degree $r$. [/step]

[step:Solve the recursive inhomogeneous transport equations]Assume that for some $j\ge 1$ the restrictions \begin{align*} c_{r}:=a_r|_{C_{\phi}\cap W},\dots,c_{r-j+1}:=a_{r-j+1}|_{C_{\phi}\cap W} \end{align*} have been constructed, are smooth, and have the required homogeneities. The symbolic hierarchy gives a smooth homogeneous source term \begin{align*} f_{r-j}:C_{\phi}\cap W\to\mathbb{C} \end{align*} and the next unknown \begin{align*} c_{r-j}:C_{\phi}\cap W\to\mathbb{C} \end{align*} must satisfy \begin{align*} \mathcal{T}_{r-j}c_{r-j}=f_{r-j},\qquad c_{r-j}|_{C_0}=b_{r-j}. \end{align*} Define \begin{align*} \Gamma_{r-j}:I\times C_0\to\mathbb{C},\qquad \Gamma_{r-j}(s,\rho_0)=\gamma_{r-j}(F(s,\rho_0)) \end{align*} and \begin{align*} G_{r-j}:I\times C_0\to\mathbb{C},\qquad G_{r-j}(s,\rho_0)=f_{r-j}(F(s,\rho_0)). \end{align*} For each $\rho_0\in C_0$, the flow-line equation is \begin{align*} \frac{d u}{ds}(s)+\Gamma_{r-j}(s,\rho_0)u(s)=G_{r-j}(s,\rho_0),\qquad u(0)=b_{r-j}(\rho_0). \end{align*} The variation-of-constants formula gives the unique solution \begin{align*} c_{r-j}(F(s,\rho_0))=\exp\left(-\int_0^s\Gamma_{r-j}(\sigma,\rho_0)\,d\mathcal{L}^1(\sigma)\right)b_{r-j}(\rho_0)+\int_0^s E_{r-j}(s,\sigma,\rho_0)G_{r-j}(\sigma,\rho_0)\,d\mathcal{L}^1(\sigma), \end{align*} where the evolution factor is the map \begin{align*} E_{r-j}:I\times I\times C_0\to\mathbb{C} \end{align*} defined by \begin{align*} E_{r-j}(s,\sigma,\rho_0):=\exp\left(-\int_{\sigma}^{s}\Gamma_{r-j}(\lambda,\rho_0)\,d\mathcal{L}^1(\lambda)\right). \end{align*} This defines a smooth homogeneous function $c_{r-j}$ of degree $r-j$ on $C_{\phi}\cap W$. Induction over $j\in\mathbb{N}_0$ therefore constructs all restrictions \begin{align*} c_{r-j}=a_{r-j}|_{C_{\phi}\cap W}. \end{align*}[/step]

[guided]At the $j$th stage, all higher homogeneous terms have already been chosen. The symbolic calculus has then converted the requirement that the coefficient of degree $r+m-j$ vanish into a first-order equation for only the next unknown coefficient. We write this unknown as \begin{align*} c_{r-j}:C_{\phi}\cap W\to\mathbb{C}. \end{align*} The equation has the form \begin{align*} \mathcal{T}_{r-j}c_{r-j}=f_{r-j},\qquad c_{r-j}|_{C_0}=b_{r-j}, \end{align*} where \begin{align*} \mathcal{T}_{r-j}c=Vc+\gamma_{r-j}c. \end{align*} The source term $f_{r-j}$ is already known because it depends only on the previously constructed functions $c_r,\dots,c_{r-j+1}$. Now use the flow coordinates \begin{align*} F:I\times C_0\to C_{\phi}\cap W. \end{align*} For a fixed starting point $\rho_0\in C_0$, the curve $s\mapsto F(s,\rho_0)$ is the integral curve of $V$. Therefore, if \begin{align*} u:I\to\mathbb{C},\qquad u(s)=c_{r-j}(F(s,\rho_0)), \end{align*} then the derivative of $u$ is \begin{align*} \frac{d u}{ds}(s)=(Vc_{r-j})(F(s,\rho_0)). \end{align*} The transport equation becomes the ordinary differential equation \begin{align*} \frac{d u}{ds}(s)+\Gamma_{r-j}(s,\rho_0)u(s)=G_{r-j}(s,\rho_0), \end{align*} where \begin{align*} \Gamma_{r-j}(s,\rho_0)=\gamma_{r-j}(F(s,\rho_0)) \end{align*} and \begin{align*} G_{r-j}(s,\rho_0)=f_{r-j}(F(s,\rho_0)). \end{align*} The prescribed Cauchy data impose \begin{align*} u(0)=b_{r-j}(\rho_0). \end{align*} The integrating factor method gives the unique solution. Define \begin{align*} E_{r-j}(s,\sigma,\rho_0):=\exp\left(-\int_{\sigma}^{s}\Gamma_{r-j}(\lambda,\rho_0)\,d\mathcal{L}^1(\lambda)\right). \end{align*} Then \begin{align*} c_{r-j}(F(s,\rho_0))=E_{r-j}(s,0,\rho_0)b_{r-j}(\rho_0)+\int_0^s E_{r-j}(s,\sigma,\rho_0)G_{r-j}(\sigma,\rho_0)\,d\mathcal{L}^1(\sigma). \end{align*} This formula proves existence and uniqueness along each bicharacteristic. Since the map $F$ is a diffeomorphism, the values along all flow lines define a unique function on the whole critical set $C_{\phi}\cap W$. Smoothness follows from smooth dependence of solutions of linear ordinary differential equations on parameters. Homogeneity is preserved because the flow, the source term, the initial data, and the transport operator all respect the conic scaling.[/guided]

[step:Extend the critical-set solutions to homogeneous amplitude coefficients] For each $j\in\mathbb{N}_0$, we have constructed a smooth homogeneous function \begin{align*} c_{r-j}:C_{\phi}\cap W\to\mathbb{C} \end{align*} of degree $r-j$. By the extension hypothesis in the statement, choose an open conic neighbourhood $W_1\subset U\times\Gamma$ of $C_{\phi}\cap W$ whose closure is contained in $W$. Since $\phi$ is nondegenerate, $C_{\phi}\cap W$ is an embedded conic submanifold of $W_1$. The support-compatible extension property applies to this embedded conic submanifold and to the homogeneous function $c_{r-j}$: it gives a smooth homogeneous function \begin{align*} a_{r-j}:U\times\Gamma\to\mathbb{C} \end{align*} of degree $r-j$ such that \begin{align*} a_{r-j}|_{C_{\phi}\cap W}=c_{r-j}. \end{align*} Choose a smooth conic cutoff \begin{align*} \zeta:U\times\Gamma\to[0,1] \end{align*} homogeneous of degree $0$, equal to $1$ on a conic neighbourhood of $C_{\phi}\cap W$ contained in $W_1$, and with conic support contained in $W$. Such a cutoff is part of the support-compatible extension hypothesis in the statement, using the inclusion of the closure of $W_1$ in $W$. Replacing $a_{r-j}$ by $\zeta a_{r-j}$ preserves the restriction to $C_{\phi}\cap W$ and gives conic support in $W$. [/step]

[step:Assemble the homogeneous coefficients by classical Borel summation] The sequence \begin{align*} (a_{r-j})_{j\in\mathbb{N}_0} \end{align*} consists of smooth functions on $U\times\Gamma$, with $a_{r-j}$ homogeneous of degree $r-j$ and conic support contained in $W$. By standard support-preserving classical Borel summation, applied to the displayed sequence of homogeneous coefficients with common conic support in $W$ and followed by a base cutoff giving local proper support in $U$, there exists an amplitude \begin{align*} a\in S^r_{\mathrm{cl}}(U\times\Gamma) \end{align*} with local proper support in $U$, conic support contained in $W$, and asymptotic expansion \begin{align*} a\sim\sum_{j=0}^{\infty}a_{r-j}. \end{align*} By construction, \begin{align*} a_{r-j}|_{C_0}=c_{r-j}|_{C_0}=b_{r-j} \end{align*} for every $j\in\mathbb{N}_0$. [/step]

[step:Show that the residual is microlocally smooth on the Lagrangian patch] Let \begin{align*} Q_{\phi}(a)\in S^{r+m}_{\mathrm{cl}}(U\times\Gamma) \end{align*} be the amplitude satisfying \begin{align*} P I_{\phi}(a)=I_{\phi}(Q_{\phi}(a)) \end{align*} microlocally on the chosen conic patch. The recursive construction made every homogeneous coefficient of $Q_{\phi}(a)$ restrict to zero on $C_{\phi}\cap W$. The phase $\phi$ is real and nondegenerate, and $Q_{\phi}(a)$ is a classical amplitude in the same conic patch. Therefore the standard coefficientwise local wave-front criterion for nondegenerate phase parametrizations applies directly: vanishing of all homogeneous coefficient restrictions on $C_{\phi}\cap W$ implies that the corresponding oscillatory integral contributes no wave front on the parametrized Lagrangian patch. Applying this criterion to $Q_{\phi}(a)$ gives \begin{align*} \operatorname{WF}(I_{\phi}(Q_{\phi}(a)))\cap\Lambda=\varnothing. \end{align*} Since $P I_{\phi}(a)=I_{\phi}(Q_{\phi}(a))$ microlocally near $\Lambda$, it follows that \begin{align*} \operatorname{WF}(P I_{\phi}(a))\cap\Lambda=\varnothing. \end{align*} [/step]

[step:Prove uniqueness of the restrictions on the critical set] Let $\widetilde a\in S^r_{\mathrm{cl}}(U\times\Gamma)$ be another amplitude satisfying the same conclusions, and write \begin{align*} \widetilde a\sim\sum_{j=0}^{\infty}\widetilde a_{r-j}. \end{align*} Define \begin{align*} d_{r-j}:=(a_{r-j}-\widetilde a_{r-j})|_{C_{\phi}\cap W}. \end{align*} Because both $P I_\phi(a)$ and $P I_\phi(\widetilde a)$ are microlocally smooth on $\Lambda$, the converse direction of the coefficientwise wave-front criterion in the statement forces the homogeneous coefficients of $Q_\phi(a)$ and $Q_\phi(\widetilde a)$ to restrict to zero on $C_\phi\cap W$ at every order. Thus, at leading order, both $a_r$ and $\widetilde a_r$ satisfy the same homogeneous transport equation and the same initial condition on $C_0$, so \begin{align*} \mathcal{T}_r d_r=0,\qquad d_r|_{C_0}=0. \end{align*} Solving this equation along the flow lines of $V$ gives $d_r=0$ on $C_{\phi}\cap W$. Assume inductively that $d_r=\cdots=d_{r-j+1}=0$ on $C_{\phi}\cap W$. At order $r-j$, the source terms in the two recursive transport equations agree because they depend only on the previous restrictions. Hence \begin{align*} \mathcal{T}_{r-j}d_{r-j}=0,\qquad d_{r-j}|_{C_0}=0. \end{align*} The unique solution of this linear ordinary differential equation along each flow line is zero, so \begin{align*} d_{r-j}=0 \end{align*} on $C_{\phi}\cap W$. Induction over $j\in\mathbb{N}_0$ proves \begin{align*} (a_{r-j}-\widetilde a_{r-j})|_{C_{\phi}\cap W}=0 \end{align*} for every $j\in\mathbb{N}_0$. This is exactly the asserted uniqueness of the recursively determined restrictions, and the proof is complete. [/step]