[proofplan] The proof is local and microlocal. We write the Schwartz kernels of $A$ and $B$ in local oscillatory-integral form, compose the kernels by integrating over the intermediate variable $y$, and observe that the resulting phase is the sum of the two original phases. The stationary equations for this summed phase encode exactly the fibre product $C_1 \times_{T^*Y} C_2$, while transversality and the embeddedness assumption make the projected critical set a nondegenerate parametrization of $C_1 \circ C_2$. Stationary phase then gives the order $m_1+m_2$ in the chosen half-density convention and identifies the leading half-density with the contracted product of the two principal symbols. [/proofplan]

[step:Localize the kernels and choose nondegenerate phase parametrizations] Fix a point of the microlocal support of the composed kernel. Choose coordinate neighbourhoods $U_X \subset X$, $U_Y \subset Y$, and $U_Z \subset Z$, and choose conic coordinate patches in the phase variables. On these patches, the Schwartz kernel $K_A$ of $A$ is represented, modulo a smooth kernel, by an oscillatory integral with a nondegenerate homogeneous phase \begin{align*} \phi_1: U_X \times U_Y \times \Gamma_1 \to \mathbb{R}, \end{align*} where $\Gamma_1 \subset \mathbb{R}^{N_1} \setminus \{0\}$ is an open conic set, and amplitude \begin{align*} a_1: U_X \times U_Y \times \Gamma_1 \to \Omega^{1/2}_{U_X \times U_Y} \end{align*} of operator order $m_1$ in the half-density convention. Thus locally \begin{align*} K_A(x,y) = \int_{\Gamma_1} e^{i\phi_1(x,y,\theta)} a_1(x,y,\theta) \, d\mathcal{L}^{N_1}(\theta). \end{align*} Similarly, the Schwartz kernel $K_B$ of $B$ is represented, modulo a smooth kernel, by a nondegenerate homogeneous phase \begin{align*} \phi_2: U_Y \times U_Z \times \Gamma_2 \to \mathbb{R}, \end{align*} where $\Gamma_2 \subset \mathbb{R}^{N_2} \setminus \{0\}$ is an open conic set, and amplitude \begin{align*} a_2: U_Y \times U_Z \times \Gamma_2 \to \Omega^{1/2}_{U_Y \times U_Z} \end{align*} of operator order $m_2$. Hence locally \begin{align*} K_B(y,z) = \int_{\Gamma_2} e^{i\phi_2(y,z,\tau)} a_2(y,z,\tau) \, d\mathcal{L}^{N_2}(\tau). \end{align*} The nondegeneracy of $\phi_1$ means that the critical set $\partial_\theta \phi_1 = 0$ is a smooth conic manifold and the map \begin{align*} (x,y,\theta) \mapsto (x,\partial_x \phi_1(x,y,\theta),y,-\partial_y \phi_1(x,y,\theta)) \end{align*} parametrizes $C_1$ on the chosen patch, with the sign in the $Y$ covector coming from the twisted convention for operator kernels. Likewise, $\phi_2$ parametrizes $C_2$ by \begin{align*} (y,z,\tau) \mapsto (y,\partial_y \phi_2(y,z,\tau),z,-\partial_z \phi_2(y,z,\tau)). \end{align*} [/step]

[step:Use proper support to form the composed kernel microlocally] Because $A$ and $B$ are properly supported, the operator composition is represented locally by the integral of the product of their kernels over the intermediate manifold $Y$. On the chosen coordinate patch, the composed kernel is therefore \begin{align*} K_{AB}(x,z) = \int_{U_Y} K_A(x,y)K_B(y,z) \, d\mathcal{L}^{\dim Y}(y), \end{align*} with the half-density factors contracted in the $Y$ variable. Substituting the two oscillatory representations gives, modulo a smooth kernel, \begin{align*} K_{AB}(x,z) = \int_{U_Y \times \Gamma_1 \times \Gamma_2} e^{i\Phi(x,y,z,\theta,\tau)} a_1(x,y,\theta)a_2(y,z,\tau) \, d\mathcal{L}^{\dim Y}(y)d\mathcal{L}^{N_1}(\theta)d\mathcal{L}^{N_2}(\tau), \end{align*} where the summed phase \begin{align*} \Phi: U_X \times U_Y \times U_Z \times \Gamma_1 \times \Gamma_2 \to \mathbb{R} \end{align*} is defined by \begin{align*} \Phi(x,y,z,\theta,\tau) := \phi_1(x,y,\theta)+\phi_2(y,z,\tau). \end{align*} The assumed properness of the projection on the relevant conic supports ensures that no uncontrolled escape in $y$, $\theta$, or $\tau$ occurs on the microlocal region considered; hence the above oscillatory integral is a legitimate local representation of the composed kernel. [/step]

[step:Identify the stationary equations with the transversal fibre product]For fixed $(x,z)$, the phase variables in the composed kernel are $(y,\theta,\tau)$. The critical equations are \begin{align*} \partial_\theta \phi_1(x,y,\theta)=0. \end{align*} \begin{align*} \partial_\tau \phi_2(y,z,\tau)=0. \end{align*} \begin{align*} \partial_y \phi_1(x,y,\theta)+\partial_y \phi_2(y,z,\tau)=0. \end{align*} The first equation says that $(x,\partial_x\phi_1,y,-\partial_y\phi_1)$ lies in $C_1$. The second says that $(y,\partial_y\phi_2,z,-\partial_z\phi_2)$ lies in $C_2$. The third equation is precisely the matching condition for the intermediate covector: \begin{align*} -\partial_y\phi_1(x,y,\theta)=\partial_y\phi_2(y,z,\tau). \end{align*} Thus the critical set of $\Phi$ in the variables $(y,\theta,\tau)$ is naturally identified with the local fibre product $C_1 \times_{T^*Y} C_2$.[/step]

[guided]We now explain why the summed phase contains exactly the geometry of canonical-relation composition. The composed kernel is obtained by multiplying $K_A(x,y)$ and $K_B(y,z)$ and then integrating out $y$. Therefore the total oscillation is governed by the phase \begin{align*} \Phi(x,y,z,\theta,\tau) := \phi_1(x,y,\theta)+\phi_2(y,z,\tau). \end{align*} The remaining phase variables are $y$, $\theta$, and $\tau$, because $x$ and $z$ are the external kernel variables. A point contributes to the associated canonical relation only when the phase is stationary in all internal variables. Stationarity in $\theta$ gives \begin{align*} \partial_\theta \phi_1(x,y,\theta)=0, \end{align*} so the nondegenerate phase $\phi_1$ produces the point \begin{align*} (x,\partial_x\phi_1(x,y,\theta),y,-\partial_y\phi_1(x,y,\theta)) \in C_1. \end{align*} Stationarity in $\tau$ gives \begin{align*} \partial_\tau \phi_2(y,z,\tau)=0, \end{align*} so the nondegenerate phase $\phi_2$ produces the point \begin{align*} (y,\partial_y\phi_2(y,z,\tau),z,-\partial_z\phi_2(y,z,\tau)) \in C_2. \end{align*} It remains to interpret the $y$-stationarity equation. Since $y$ is the variable being integrated out, stationary phase requires \begin{align*} \partial_y \Phi(x,y,z,\theta,\tau)=0. \end{align*} By the definition of $\Phi$, this is \begin{align*} \partial_y \phi_1(x,y,\theta)+\partial_y \phi_2(y,z,\tau)=0. \end{align*} Equivalently, \begin{align*} -\partial_y\phi_1(x,y,\theta)=\partial_y\phi_2(y,z,\tau). \end{align*} The covector on the $Y$ side of $C_1$ is $-\partial_y\phi_1$, while the covector on the $Y$ side of $C_2$ is $\partial_y\phi_2$. Thus this equation is exactly the condition that the intermediate covectors agree. Consequently, the critical set of $\Phi$ in the variables $(y,\theta,\tau)$ is the local model for \begin{align*} C_1 \times_{T^*Y} C_2. \end{align*} This is the geometric reason that the product phase parametrizes the composition rather than some unrelated relation.[/guided]

[step:Use transversality to obtain a nondegenerate phase for the composed relation] By hypothesis, $C_1$ and $C_2$ meet transversally over $T^*Y \setminus 0$. Therefore the fibre product $C_1 \times_{T^*Y} C_2$ is a smooth conic manifold of the expected dimension, with excess zero. The additional hypothesis that the projection \begin{align*} C_1 \times_{T^*Y} C_2 \to T^*X \setminus 0 \times T^*Z \setminus 0 \end{align*} has embedded image on the microlocal region considered implies that this image is precisely the embedded conic canonical relation $C_1 \circ C_2$. Under the local identification from the previous step, these hypotheses say that the critical set of $\Phi$ in the variables $(y,\theta,\tau)$ is clean with excess zero and that the induced map \begin{align*} (x,y,z,\theta,\tau) \mapsto (x,\partial_x\Phi(x,y,z,\theta,\tau),z,-\partial_z\Phi(x,y,z,\theta,\tau)) \end{align*} has image $C_1 \circ C_2$. Since \begin{align*} \partial_x\Phi=\partial_x\phi_1 \end{align*} and \begin{align*} \partial_z\Phi=\partial_z\phi_2, \end{align*} this image is \begin{align*} (x,\partial_x\phi_1(x,y,\theta),z,-\partial_z\phi_2(y,z,\tau)), \end{align*} with $(y,\theta,\tau)$ satisfying the critical equations. Thus $\Phi$, after eliminating redundant internal variables by the implicit-function theorem, gives a nondegenerate homogeneous phase parametrizing $C_1 \circ C_2$. [/step]

[step:Apply stationary phase and track the operator order] We apply the [stationary phase theorem](/theorems/8198) for clean nondegenerate oscillatory integrals with excess zero, citing a result not yet in the wiki: Stationary phase theorem for oscillatory integrals. Its hypotheses are satisfied because the preceding step gives a clean critical set of excess zero, the amplitudes are classical symbols on the chosen conic patches, and the properness assumption gives microlocal compactness in the internal variables after conic localization. Stationary phase in the internal variables transverse to the critical set replaces the integral over $(y,\theta,\tau)$ by an oscillatory integral whose phase parametrizes $C_1 \circ C_2$. In the half-density operator-order convention fixed in the statement, the stationary phase normalization exactly cancels the density contribution from the transverse Hessian in the excess-zero case. Therefore the resulting amplitude has operator order \begin{align*} m_1+m_2. \end{align*} Consequently, \begin{align*} AB \in I^{m_1+m_2}(X,Z;C_1 \circ C_2) \end{align*} microlocally on the chosen patch. Since the argument is invariant under changes of local phase parametrization and the patches cover the relevant conic support, the inclusion holds globally on the stated microlocal region. [/step]

[step:Identify the leading symbol by half-density contraction] Let $\sigma(A)$ and $\sigma(B)$ denote the principal symbols of $A$ and $B$ as half-densities on $C_1$ and $C_2$, including the chosen Maslov factors. On the fibre product $C_1 \times_{T^*Y} C_2$, their exterior product is a half-density \begin{align*} \sigma(A)\boxtimes\sigma(B) \end{align*} on the product relation restricted to the matching intermediate covector. The leading term in stationary phase is the product of the leading amplitudes $a_1$ and $a_2$ multiplied by the inverse square root of the transverse Hessian density and by the convention-dependent Maslov phase. With the standard half-density identifications fixed in the statement, this stationary-phase density is exactly the canonical contraction of half-densities along the transversal fibre over $T^*Y$. Hence the principal symbol of the composed operator is \begin{align*} \sigma(AB)=\operatorname{Contr}_{T^*Y}(\sigma(A)\boxtimes\sigma(B)), \end{align*} where $\operatorname{Contr}_{T^*Y}$ denotes the half-density contraction induced by the projection \begin{align*} C_1 \times_{T^*Y} C_2 \to C_1 \circ C_2. \end{align*} This is precisely multiplication of the two principal symbols followed by contraction along the transversal fibre, completing the proof. [/step]