[proofplan] The proof is microlocal and takes place after shrinking the conic neighbourhoods so that the canonical relation is a single elliptic canonical graph. The implication from observed regularity to source regularity uses the elliptic Fourier integral parametrix: an inverse-graph operator $B$ makes $BA$ an elliptic pseudodifferential operator on $\Gamma_X$, and pseudodifferential elliptic regularity recovers $u$. The converse decomposes the source into the selected branch and its microlocal complement; the wave front mapping theorem controls the selected branch, while the branch-exclusion hypothesis prevents singularities from the complement from reaching $\Gamma_Y$. The same argument with Sobolev wave front sets gives the stated order-shifted Sobolev equivalence. [/proofplan] [step:Shrink the conic neighbourhoods and choose microlocal cutoffs] Choose conic open neighbourhoods \begin{align*} \Gamma_X'\subset \Gamma_X \end{align*} of $q_X$ and \begin{align*} \Gamma_Y'\subset \Gamma_Y \end{align*} of $q_Y$ such that \begin{align*} \kappa(\Gamma_X')=\Gamma_Y', \end{align*} the graph identity \begin{align*} C\cap(\Gamma_Y'\times \Gamma_X')=\operatorname{graph}(\kappa|_{\Gamma_X'}) \end{align*} holds, the principal symbol of $A$ is elliptic on this graph, and \begin{align*} C\cap\bigl(\Gamma_Y'\times (T^*X\setminus 0)\bigr) = C\cap(\Gamma_Y'\times \Gamma_X'). \end{align*} Since microlocal regularity in $\Gamma_X$ and $\Gamma_Y$ is local in the conic topology, it is enough to prove the equivalence on such smaller neighbourhoods and then cover the original neighbourhoods by them. Let $P_X\in \Psi^0_{\mathrm{prop}}(X)$ be a properly supported pseudodifferential cutoff whose principal symbol is equal to $1$ on a conic neighbourhood of $\overline{\Gamma_X'}$ and whose microsupport is contained in $\Gamma_X$. Let $P_Y\in \Psi^0_{\mathrm{prop}}(Y)$ be a properly supported pseudodifferential cutoff whose principal symbol is equal to $1$ on a conic neighbourhood of $\overline{\Gamma_Y'}$ and whose microsupport is contained in $\Gamma_Y$. These cutoffs localize the source and target to the single elliptic branch. [/step] [step:Construct an inverse-graph parametrix for the elliptic branch] By the [microlocal parametrix theorem for elliptic Fourier integral operators](/theorems/8211) associated to canonical graphs, applied to the [elliptic operator](/page/Elliptic%20Operator) $A$ on the graph of \begin{align*} \kappa:\Gamma_X'\to \Gamma_Y', \end{align*} there exists a properly supported Fourier integral operator \begin{align*} B:\mathcal{D}'(Y)\to \mathcal{D}'(X) \end{align*} associated with the inverse canonical graph \begin{align*} \operatorname{graph}(\kappa^{-1})\subset \Gamma_X'\times \Gamma_Y' \end{align*} such that $BA$ is microlocally equal on $\Gamma_X'$ to a properly supported pseudodifferential operator \begin{align*} E\in \Psi^0_{\mathrm{prop}}(X) \end{align*} whose principal symbol is elliptic on $\Gamma_X'$. This uses the [clean composition theorem for properly supported Fourier integral operators](/theorems/8209), because the graph of $\kappa^{-1}$ and the graph of $\kappa$ compose transversally and cleanly to the diagonal canonical relation over $\Gamma_X'$. Thus there exists a smoothing remainder \begin{align*} R:\mathcal{D}'(X)\to C^\infty(X) \end{align*} microlocally near $\Gamma_X'$ such that \begin{align*} BAu=Eu+Ru \end{align*} microlocally in $\Gamma_X'$ for every $u\in\mathcal{D}'(X)$. [guided] The goal of this step is to turn the Fourier integral operator into something elliptic on the original source cotangent variables. The hypothesis that $C$ is a graph is exactly what makes this possible: near the chosen branch, each source covector in $\Gamma_X'$ corresponds to exactly one observed covector in $\Gamma_Y'$ through the canonical diffeomorphism \begin{align*} \kappa:\Gamma_X'\to \Gamma_Y'. \end{align*} Since the principal symbol of $A$ is elliptic on $\operatorname{graph}(\kappa)$, the microlocal parametrix theorem for elliptic Fourier integral operators gives a properly supported Fourier integral operator \begin{align*} B:\mathcal{D}'(Y)\to \mathcal{D}'(X) \end{align*} whose canonical relation is the inverse graph \begin{align*} \operatorname{graph}(\kappa^{-1})\subset \Gamma_X'\times \Gamma_Y'. \end{align*} The role of $B$ is to pull observed singularities back from $Y$ to $X$ along the inverse canonical transformation. We now compose $B$ with $A$. The canonical relation of $A$ is the graph of $\kappa$, while the canonical relation of $B$ is the graph of $\kappa^{-1}$. Their composition is the diagonal relation over $\Gamma_X'$, because \begin{align*} \kappa^{-1}(\kappa(q))=q \end{align*} for every $q\in\Gamma_X'$. The clean composition theorem for properly supported Fourier integral operators therefore identifies $BA$ microlocally near $\Gamma_X'$ with a properly supported pseudodifferential operator \begin{align*} E\in \Psi^0_{\mathrm{prop}}(X). \end{align*} Ellipticity of the principal symbol of $A$ and the reciprocal principal symbol used in the construction of $B$ imply that the principal symbol of $E$ is elliptic on $\Gamma_X'$. Consequently, for every $u\in\mathcal{D}'(X)$, there is a remainder \begin{align*} R:\mathcal{D}'(X)\to C^\infty(X) \end{align*} which is smoothing microlocally near $\Gamma_X'$ and satisfies \begin{align*} BAu=Eu+Ru \end{align*} microlocally in $\Gamma_X'$. This is the precise point at which the elliptic FIO is replaced by an elliptic pseudodifferential operator, so that pseudodifferential elliptic regularity can be used in the next step. [/guided] [/step] [step:Recover source microlocal smoothness from observed microlocal smoothness] Assume first that \begin{align*} \operatorname{WF}(Au)\cap \Gamma_Y=\varnothing. \end{align*} Since the canonical relation of $B$ is contained in $\Gamma_X'\times \Gamma_Y'$, the [wave front mapping theorem for Fourier integral operators](/theorems/8206) gives \begin{align*} \operatorname{WF}(B Au)\cap \Gamma_X'=\varnothing. \end{align*} The remainder $Ru$ is smooth microlocally in $\Gamma_X'$, hence \begin{align*} \operatorname{WF}(Eu)\cap \Gamma_X'=\varnothing. \end{align*} Because $E$ is elliptic on $\Gamma_X'$, [microlocal elliptic regularity for pseudodifferential operators](/theorems/8163) gives \begin{align*} \operatorname{WF}(u)\cap \Gamma_X'=\varnothing. \end{align*} Covering $\Gamma_X$ by such neighbourhoods proves \begin{align*} \operatorname{WF}(Au)\cap \Gamma_Y=\varnothing \implies \operatorname{WF}(u)\cap \Gamma_X=\varnothing. \end{align*} Here the elliptic regularity input is [Microlocal Elliptic Regularity Theorem]([citetheorem:8175]), applied to the elliptic pseudodifferential operator $E$. [/step] [step:Propagate regularity from the selected source branch to the observed branch] Assume conversely that \begin{align*} \operatorname{WF}(u)\cap \Gamma_X=\varnothing. \end{align*} Using the source cutoff $P_X$, decompose \begin{align*} u=P_Xu+(I-P_X)u \end{align*} microlocally near all source covectors that can reach $\Gamma_Y'$, where $I$ denotes the identity operator on $\mathcal{D}'(X)$. For the selected branch, $P_Xu$ is smooth microlocally in $\Gamma_X'$ by the assumption and by the [pseudodifferential characterization of the wave front set](/theorems/8174). The wave front mapping theorem for Fourier integral operators, applied to $A P_X$, gives \begin{align*} \operatorname{WF}(A P_Xu)\cap \Gamma_Y'=\varnothing. \end{align*} For the complementary branch, the microsupport of $I-P_X$ is disjoint from $\Gamma_X'$ near every source covector paired by $C$ with a covector in $\Gamma_Y'$. The branch-exclusion hypothesis states precisely that \begin{align*} C\cap\bigl(\Gamma_Y'\times (T^*X\setminus 0)\bigr) = C\cap(\Gamma_Y'\times \Gamma_X'). \end{align*} Therefore no element of $\operatorname{WF}((I-P_X)u)$ can be carried by $C$ into $\Gamma_Y'$. Applying the wave front mapping theorem again yields \begin{align*} \operatorname{WF}(A(I-P_X)u)\cap \Gamma_Y'=\varnothing. \end{align*} Since \begin{align*} Au=A P_Xu+A(I-P_X)u \end{align*} microlocally near $\Gamma_Y'$, the union property of wave front sets gives \begin{align*} \operatorname{WF}(Au)\cap \Gamma_Y'=\varnothing. \end{align*} Covering $\Gamma_Y$ by such neighbourhoods proves \begin{align*} \operatorname{WF}(u)\cap \Gamma_X=\varnothing \implies \operatorname{WF}(Au)\cap \Gamma_Y=\varnothing. \end{align*} The mapping theorem used here is [Wave Front Mapping Theorem for Fourier Integral Operators]([citetheorem:8206]). [/step] [step:Repeat the argument with Sobolev wave front sets and track the order shift] Let $s\in\mathbb{R}$. The Sobolev version follows by replacing $\operatorname{WF}$ throughout by $WF^s$ on $X$ and by $WF^{s-m}$ on $Y$, using the convention that an order-$m$ Fourier integral operator associated to a canonical graph maps microlocal $H^s$ regularity on the source to microlocal $H^{s-m}$ regularity on the target. For the forward implication, if \begin{align*} WF^{s-m}(Au)\cap \Gamma_Y=\varnothing, \end{align*} then the inverse operator $B$, whose order is the inverse order prescribed by the parametrix construction, gives $BAu$ microlocally in $H^s$ on $\Gamma_X'$. Since $BAu=Eu+Ru$ microlocally on $\Gamma_X'$, with $R$ smoothing and $E$ elliptic pseudodifferential of order $0$, [microlocal Sobolev elliptic regularity](/theorems/8179) gives \begin{align*} WF^s(u)\cap \Gamma_X'=\varnothing. \end{align*} This uses [Microlocal Sobolev Elliptic Regularity]([citetheorem:8179]). For the converse, if \begin{align*} WF^s(u)\cap \Gamma_X=\varnothing, \end{align*} then $P_Xu$ is microlocally $H^s$ in $\Gamma_X'$, so the Sobolev mapping property for order-$m$ Fourier integral operators gives $A P_Xu$ microlocally in $H^{s-m}$ in $\Gamma_Y'$. The complementary term $A(I-P_X)u$ is microlocally smooth in $\Gamma_Y'$ by the same branch-exclusion argument as above, and hence is also microlocally $H^{s-m}$ there. Therefore \begin{align*} WF^{s-m}(Au)\cap \Gamma_Y'=\varnothing. \end{align*} Covering the original conic neighbourhoods gives \begin{align*} WF^{s-m}(Au)\cap \Gamma_Y=\varnothing \quad\Longleftrightarrow\quad WF^s(u)\cap \Gamma_X=\varnothing. \end{align*} Together with the smooth case proved above, this completes the proof. [/step]