[proofplan] We prove the theorem locally, because membership in an FIO class and the principal symbol are local on the source and target manifolds, while proper support allows the local pieces to be summed without changing the canonical relation. In local coordinates the kernels of $A$ and $B$ are oscillatory integrals with phases parametrising $C_1$ and $C_2$; the kernel of $AB$ is obtained by integrating their product over the intermediate variable on $Y$. The clean fibre-product hypothesis identifies the critical manifold of the composed phase with $F$ and identifies the null directions of the Hessian with the clean excess. The clean [stationary phase theorem](/theorems/8198) then gives the order shift $e/2$, and its leading term is exactly fibre integration of the product of the two principal symbols, with the Maslov factor supplied by clean reduction. [/proofplan]

[step:Write local oscillatory representations for the two kernels] Fix coordinate charts on $X$, $Y$, and $Z$, and let $n_Y := \dim Y$. Let $N_1,N_2 \in \mathbb{N}$ denote the numbers of homogeneous phase variables used in the local parametrizations of $C_1$ and $C_2$, respectively. Since $A \in I^{m_1}(X,Y;C_1)$ and $B \in I^{m_2}(Y,Z;C_2)$, their Schwartz kernels, written in these coordinate charts and acting on half-densities, are locally finite sums of oscillatory integrals of the form \begin{align*} K_A(x,y) = \int_{\mathbb{R}^{N_1}} e^{i\phi_1(x,y,\theta)} a(x,y,\theta) \, d\mathcal{L}^{N_1}(\theta) \end{align*} and \begin{align*} K_B(y,z) = \int_{\mathbb{R}^{N_2}} e^{i\phi_2(y,z,\tau)} b(y,z,\tau) \, d\mathcal{L}^{N_2}(\tau). \end{align*} Here $\phi_1$ and $\phi_2$ are nondegenerate homogeneous phase functions parametrising $C_1$ and $C_2$ in the stated canonical-relation convention, while $a$ and $b$ are classical half-density amplitudes of the orders prescribed by the standard half-density FIO normalization: an oscillatory integral with $N_j$ homogeneous phase variables and amplitude order $\mu_j$ represents an element of $I^{m_j}$ exactly when $m_j$ is the corresponding FIO order under that normalization. This is the same normalization used below in the clean stationary phase order shift. The phrase “parametrising $C_1$” means that the critical set of $\phi_1$ in the $\theta$ variables maps to $C_1$ by \begin{align*} (x,y,\theta) \mapsto (x,\partial_x\phi_1(x,y,\theta),y,-\partial_y\phi_1(x,y,\theta)), \end{align*} with the sign in the $Y$ covector absorbed by the canonical-relation convention. Similarly, the critical set of $\phi_2$ in the $\tau$ variables maps to $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:Express the composed kernel by integrating over the intermediate manifold] Because $A$ and $B$ are properly supported, the composition kernel is locally given by the fibrewise contraction of half-densities over the intermediate variable $y \in Y$. In the chosen coordinate chart on $Y$, this is \begin{align*} K_{AB}(x,z) = \int_Y K_A(x,y)K_B(y,z)\,d\mathcal{L}^{n_Y}(y). \end{align*} After inserting compactly supported cutoffs in the coordinate charts and interpreting each oscillatory integral by the usual regularization, proper support gives a compact set of $y$ values for $(x,z)$ in a compact coordinate patch. The standard [Fubini theorem](/theorems/513) for properly supported oscillatory kernels therefore permits the $y$, $\theta$, and $\tau$ integrations to be combined, giving \begin{align*} K_{AB}(x,z) = \int_{Y \times \mathbb{R}^{N_1} \times \mathbb{R}^{N_2}} e^{i\Phi(x,y,z,\theta,\tau)} a(x,y,\theta)b(y,z,\tau)\,d\mathcal{L}^{n_Y}(y)d\mathcal{L}^{N_1}(\theta)d\mathcal{L}^{N_2}(\tau), \end{align*} where the composed phase is the smooth homogeneous function \begin{align*} \Phi:X \times Y \times Z \times \mathbb{R}^{N_1}_0 \times \mathbb{R}^{N_2}_0 \to \mathbb{R}, \qquad \Phi(x,y,z,\theta,\tau)=\phi_1(x,y,\theta)+\phi_2(y,z,\tau). \end{align*} Proper support is used here to ensure that, after inserting a [partition of unity](/page/Partition%20of%20Unity), the integration in $y$ is over a compact subset of the chosen coordinate chart whenever $(x,z)$ ranges in a compact coordinate patch. [/step]

[step:Identify the critical manifold of the composed phase with the clean fibre product]Let $\mathcal{C}_\Phi$ denote the critical set of $\Phi$ in the variables $(y,\theta,\tau)$: \begin{align*} \mathcal{C}_\Phi := \{(x,y,z,\theta,\tau): \partial_y\Phi=0,\ \partial_\theta\Phi=0,\ \partial_\tau\Phi=0\}. \end{align*} The equations $\partial_\theta\Phi=0$ and $\partial_\tau\Phi=0$ say exactly that $(x,y,\theta)$ and $(y,z,\tau)$ lie on the critical sets of the two phase functions. The remaining equation is \begin{align*} \partial_y\phi_1(x,y,\theta)+\partial_y\phi_2(y,z,\tau)=0, \end{align*} which is precisely the equality of the intermediate covectors in $T^*Y \setminus 0$ under the sign convention for kernels. Therefore the parametrization maps identify $\mathcal{C}_\Phi$ with the fibre product $F$. Under this identification, the map from the critical set to the outgoing canonical relation is the map $p:F \to C_1 \circ C_2$.[/step]

[guided]The composed phase has three kinds of internal variables: the intermediate base point $y \in Y$, the phase variable $\theta \in \mathbb{R}^{N_1}_0$ for $A$, and the phase variable $\tau \in \mathbb{R}^{N_2}_0$ for $B$. Thus the relevant critical equations are not the full critical equations in $(x,z)$, but the equations in the variables being integrated out: \begin{align*} \partial_y\Phi=0,\qquad \partial_\theta\Phi=0,\qquad \partial_\tau\Phi=0. \end{align*} Since $\Phi=\phi_1+\phi_2$, the equations in the phase variables are \begin{align*} \partial_\theta\phi_1(x,y,\theta)=0 \end{align*} and \begin{align*} \partial_\tau\phi_2(y,z,\tau)=0. \end{align*} These equations put $(x,y,\theta)$ on the critical set parametrising $C_1$ and $(y,z,\tau)$ on the critical set parametrising $C_2$. The covector over $Y$ contributed by the first kernel is represented, with the kernel sign convention, by $-\partial_y\phi_1(x,y,\theta)$, while the covector over $Y$ contributed by the second kernel is represented by $\partial_y\phi_2(y,z,\tau)$. The remaining critical equation \begin{align*} \partial_y\Phi(x,y,z,\theta,\tau)=\partial_y\phi_1(x,y,\theta)+\partial_y\phi_2(y,z,\tau)=0 \end{align*} therefore says that these two intermediate covectors agree. Consequently a point of $\mathcal{C}_\Phi$ is exactly the same local datum as a triple $(\rho_X,\rho_Y,\rho_Z)$ satisfying $(\rho_X,\rho_Y)\in C_1$ and $(\rho_Y,\rho_Z)\in C_2$. This is the fibre product $F$. The projection from the critical set to the external covectors keeps only the $X$ and $Z$ covectors, so it is precisely the map \begin{align*} p:F \to (T^*X\setminus 0)\times (T^*Z\setminus 0), \qquad p(\rho_X,\rho_Y,\rho_Z)=(\rho_X,\rho_Z). \end{align*}[/guided]

[step:Apply clean stationary phase in the normal directions] The clean-intersection hypothesis says that $F$ is a smooth manifold and that its tangent space is the fibre product of $TC_1$ and $TC_2$ over $T(T^*Y\setminus 0)$. In phase-function terms, this is exactly the statement that $\mathcal{C}_\Phi$ is a clean critical manifold and that the kernel of the Hessian of $\Phi$ in the integrated variables $(y,\theta,\tau)$ is $T\mathcal{C}_\Phi$. We apply the clean stationary phase theorem to the oscillatory integral defining $K_{AB}$ in the variables $(y,\theta,\tau)$. The hypotheses required by that theorem are satisfied: the critical set is smooth by cleanness, the Hessian is nondegenerate on the normal bundle to the critical set by the clean tangent-space identity, and the support in the integrated variables is proper by the assumed proper support of the kernels and the properness of $p$ on the relevant conic support. Hence $K_{AB}$ is a Lagrangian distribution associated to the image $p(F)=C_1\circ C_2$. The same theorem gives the order shift. Since the clean fibres have dimension $e$, stationary phase is performed only in the nondegenerate normal directions and leaves an $e$-dimensional fibre integral. Under the standard FIO order convention for half-densities, this changes the order by $e/2$, so \begin{align*} K_{AB} \in I^{m_1+m_2+e/2}(X \times Z; C_1\circ C_2). \end{align*} Equivalently, \begin{align*} AB \in I^{m_1+m_2+e/2}(X,Z;C_1\circ C_2). \end{align*} Here we are using the following standard clean stationary phase theorem for half-density oscillatory integrals: if a homogeneous phase has a clean critical manifold, the Hessian is nondegenerate on the normal bundle, and the projection to the outgoing Lagrangian has clean fibres of dimension $e$, then the integral is a Lagrangian distribution whose principal coefficient is obtained by integrating the induced vertical half-density over those fibres, and under the standard half-density FIO normalization its FIO order is increased by $e/2$ relative to the transverse nondegenerate composition case. [/step]

[step:Use properness and embeddedness to globalize the local Lagrangian distribution] The local construction above is compatible on overlaps because changes of phase function transform amplitudes by the standard half-density and Maslov transition factors. The assumption that $p$ is proper on the conic support ensures that no noncompact family of intermediate points in $T^*Y\setminus 0$ contributes to a compact piece of the composed kernel. Therefore the local oscillatory integrals patch to a globally defined distributional half-density kernel on $X \times Z$. The assumption that $p(F)=C_1\circ C_2$ is an embedded conic Lagrangian submanifold ensures that the patched kernel has one canonical relation rather than an immersed or self-intersecting relation with several unresolved branches. Thus the composed operator is a properly supported Fourier integral operator associated to $C_1\circ C_2$. [/step]

[step:Compute the leading symbol by fibre integration over the clean fibres] Let $\sigma(A)$ and $\sigma(B)$ denote the principal symbols of $A$ and $B$ in the standard half-density convention. Pull them back to $F$ by the maps \begin{align*} \pi_1:F \to C_1, \qquad \pi_1(\rho_X,\rho_Y,\rho_Z)=(\rho_X,\rho_Y) \end{align*} and \begin{align*} \pi_2:F \to C_2, \qquad \pi_2(\rho_X,\rho_Y,\rho_Z)=(\rho_Y,\rho_Z). \end{align*} Their product \begin{align*} \pi_1^*\sigma(A)\,\pi_2^*\sigma(B) \end{align*} is a half-density-valued Maslov section on the clean fibre product $F$ after using the standard tensor-product pairing of the intermediate half-densities over $Y$. Clean stationary phase identifies the leading amplitude of $K_{AB}$ with the integral of this induced half-density along the clean fibre of $p$. For each point $\rho \in C_1\circ C_2$, the fibre is \begin{align*} p^{-1}(\rho) = \{q \in F : p(q)=\rho\}. \end{align*} By the constant-excess hypothesis, these fibres have dimension $e$ on the relevant conic support. The fibre-integration map \begin{align*} p_!: \text{half-density symbols on }F \to \text{half-density symbols on }C_1\circ C_2 \end{align*} is therefore well-defined by integrating the vertical half-density over $p^{-1}(\rho)$, with the Maslov-bundle factor identified by the clean reduction. Thus the principal symbol of the composed operator is \begin{align*} \sigma(AB)=p_!\bigl(\pi_1^*\sigma(A)\,\pi_2^*\sigma(B)\bigr). \end{align*} The next term in the clean stationary phase expansion has one lower symbolic degree, so this identity holds modulo symbols of order \begin{align*} m_1+m_2+e/2-1. \end{align*} This proves both the claimed FIO order and the stated principal-symbol formula. [/step]