[proofplan] The proof is local on $X \times Y \times Z$ and microlocal near the wavefront-relevant part of the clean fibre product. We write the two kernels as oscillatory integrals whose phases parametrize $C_1$ and $C_2$, multiply the kernels, and integrate over the intermediate variable $y \in Y$. The stationary equations for the combined phase impose precisely the sign condition $\eta+\eta'=0$, so the clean intersection hypothesis gives a clean critical manifold of constant excess $e$. Clean stationary phase then produces a new oscillatory integral associated with the projected image $C_1 \circ C_2$, and the chapter's kernel-order normalization gives the order \begin{align*} m_1+m_2+\frac{e}{2}. \end{align*} [/proofplan]

[step:Localize the kernels near the wavefront-relevant clean fibre product]Because $A$ and $B$ are properly supported, their composition is defined by the standard kernel composition criterion for properly supported operators (citing a result not yet in the wiki: Kernel composition criterion for properly supported operators). Thus the Schwartz kernel $K_{AB}$ is locally obtained from $K_A$ and $K_B$ by pairing over the intermediate manifold $Y$. Fix coordinate charts $(U_X,\kappa_X)$ on $X$, $(U_Y,\kappa_Y)$ on $Y$, and $(U_Z,\kappa_Z)$ on $Z$. In these charts, let \begin{align*} \phi_1: U_X \times U_Y \times (\mathbb{R}^{N_1} \setminus 0) \to \mathbb{R} \end{align*} and \begin{align*} \phi_2: U_Y \times U_Z \times (\mathbb{R}^{N_2} \setminus 0) \to \mathbb{R} \end{align*} be nondegenerate positively homogeneous phase functions parametrizing $C_1$ and $C_2$, respectively, on the chosen microlocal patches. Let \begin{align*} a_1: U_X \times U_Y \times (\mathbb{R}^{N_1} \setminus 0) \to \mathbb{C} \end{align*} and \begin{align*} a_2: U_Y \times U_Z \times (\mathbb{R}^{N_2} \setminus 0) \to \mathbb{C} \end{align*} be classical amplitudes in the precise symbol orders prescribed by the chapter's kernel-order convention for $I^{m_1}(X,Y;C_1)$ and $I^{m_2}(Y,Z;C_2)$. We write $\mathcal{L}^{N_1}$, $\mathcal{L}^{N_2}$, and $\mathcal{L}^{\dim Y}$ for [Lebesgue measure](/page/Lebesgue%20Measure) in the chosen coordinate variables. After inserting microlocal cutoffs supported in these coordinate patches, the kernels have the local form, interpreted as regularized oscillatory integrals, \begin{align*} K_A(x,y)=\int_{\mathbb{R}^{N_1}} e^{i\phi_1(x,y,\theta)} a_1(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,\sigma)} a_2(y,z,\sigma) \, d\mathcal{L}^{N_2}(\sigma), \end{align*} where $x \in U_X$, $y \in U_Y$, $z \in U_Z$, $\theta \in \mathbb{R}^{N_1} \setminus 0$, and $\sigma \in \mathbb{R}^{N_2} \setminus 0$.[/step]

[guided]We first reduce the assertion to the local oscillatory-integral calculation. Proper support is the hypothesis that prevents the intermediate integration over $Y$ from escaping to infinity: for compact sets in the outer variables, only a compact set of intermediate points $y \in Y$ contributes. Therefore the standard kernel composition criterion for properly supported operators (citing a result not yet in the wiki: Kernel composition criterion for properly supported operators) allows us to compute the composed kernel locally by multiplying the two kernels and integrating over $Y$. Choose coordinate charts $(U_X,\kappa_X)$, $(U_Y,\kappa_Y)$, and $(U_Z,\kappa_Z)$. On a conic microlocal patch of $C_1$, choose a nondegenerate positively homogeneous phase function \begin{align*} \phi_1: U_X \times U_Y \times (\mathbb{R}^{N_1} \setminus 0) \to \mathbb{R}. \end{align*} This means that the critical set of $\phi_1$ in the auxiliary variable $\theta \in \mathbb{R}^{N_1} \setminus 0$ parametrizes the relevant piece of $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*} Likewise, on a conic microlocal patch of $C_2$, choose \begin{align*} \phi_2: U_Y \times U_Z \times (\mathbb{R}^{N_2} \setminus 0) \to \mathbb{R} \end{align*} so that the corresponding parametrization is \begin{align*} (y,z,\sigma) \mapsto (y,\partial_y\phi_2(y,z,\sigma);z,\partial_z\phi_2(y,z,\sigma)). \end{align*} The amplitudes \begin{align*} a_1: U_X \times U_Y \times (\mathbb{R}^{N_1} \setminus 0) \to \mathbb{C} \end{align*} and \begin{align*} a_2: U_Y \times U_Z \times (\mathbb{R}^{N_2} \setminus 0) \to \mathbb{C} \end{align*} belong to the symbol classes corresponding to the orders $m_1$ and $m_2$ in the chapter's kernel-order convention. Thus, after microlocal cutoffs, the two kernels are represented as \begin{align*} K_A(x,y)=\int_{\mathbb{R}^{N_1}} e^{i\phi_1(x,y,\theta)} a_1(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,\sigma)} a_2(y,z,\sigma) \, d\mathcal{L}^{N_2}(\sigma). \end{align*} This localization is harmless because the desired conclusion is microlocal, and the statement assumes properness and constant rank on the closed conic subset [lying over](/theorems/2876) $\operatorname{WF}'(A)\times\operatorname{WF}'(B)$.[/guided]

[step:Write the composed kernel with the combined phase] Define the combined phase \begin{align*} \Phi: U_X \times U_Y \times U_Z \times (\mathbb{R}^{N_1} \setminus 0) \times (\mathbb{R}^{N_2} \setminus 0) \to \mathbb{R} \end{align*} by \begin{align*} \Phi(x,y,z,\theta,\sigma)=\phi_1(x,y,\theta)+\phi_2(y,z,\sigma). \end{align*} Define the product amplitude \begin{align*} a: U_X \times U_Y \times U_Z \times (\mathbb{R}^{N_1} \setminus 0) \times (\mathbb{R}^{N_2} \setminus 0) \to \mathbb{C} \end{align*} by \begin{align*} a(x,y,z,\theta,\sigma)=a_1(x,y,\theta)a_2(y,z,\sigma). \end{align*} The local expression for the composed kernel is then the regularized oscillatory integral \begin{align*} K_{AB}(x,z)=\operatorname{Os}\!\int_{U_Y}\int_{\mathbb{R}^{N_1}}\int_{\mathbb{R}^{N_2}} e^{i\Phi(x,y,z,\theta,\sigma)} a(x,y,z,\theta,\sigma) \, d\mathcal{L}^{N_2}(\sigma) \, d\mathcal{L}^{N_1}(\theta) \, d\mathcal{L}^{\dim Y}(y), \end{align*} where $\operatorname{Os}\!\int$ denotes the standard limit obtained by inserting a compactly supported cutoff in $(\theta,\sigma)$ which tends to $1$ together with all derivatives on compact conic sets. The support cutoffs and proper support ensure that the $y$-integration is over a compact subset of the coordinate patch for fixed compact subsets of $U_X \times U_Z$, while the regularized oscillatory-integral definition justifies the product and pushforward at the distributional level. [/step]

[step:Identify the stationary equations with the negative fibre product] The variables integrated out in the composed kernel are $y$, $\theta$, and $\sigma$. Hence the relevant critical equations are \begin{align*} \partial_\theta\phi_1(x,y,\theta)=0, \end{align*} \begin{align*} \partial_\sigma\phi_2(y,z,\sigma)=0, \end{align*} and \begin{align*} \partial_y\phi_1(x,y,\theta)+\partial_y\phi_2(y,z,\sigma)=0. \end{align*} On the critical set of $\partial_\theta\phi_1$ and $\partial_\sigma\phi_2$, the phase parametrizations give \begin{align*} \xi=\partial_x\phi_1(x,y,\theta), \end{align*} \begin{align*} \eta=\partial_y\phi_1(x,y,\theta), \end{align*} \begin{align*} \eta'=\partial_y\phi_2(y,z,\sigma), \end{align*} and \begin{align*} \zeta=\partial_z\phi_2(y,z,\sigma). \end{align*} Therefore the remaining stationarity equation in $y$ is exactly $\eta+\eta'=0$. Thus the critical set of $\Phi$ in the integration variables maps to \begin{align*} C_1 \times_{T^*Y}^{-} C_2. \end{align*} Conversely, every point of the fibre product lying in the chosen parametrizing patches is represented by such a critical point of $\Phi$. The clean-intersection hypothesis therefore says precisely that this critical set is a clean critical manifold of constant excess $e$. [/step]

[step:Apply clean stationary phase along the clean critical manifold]We now apply the clean [stationary phase theorem](/theorems/8198) to the phase $\Phi$ in the integration variables $(y,\theta,\sigma)$. The theorem requires a clean critical manifold and constant normal Hessian rank. These are exactly the phase-level hypotheses of this theorem: the critical set maps diffeomorphically onto the corresponding microlocal piece of $C_1 \times_{T^*Y}^{-} C_2$, and the Hessian of $\Phi$ transverse to that critical manifold has constant rank. Therefore clean stationary phase applies to the regularized oscillatory integral for $K_{AB}$. Its conclusion is that, modulo a smooth kernel, $K_{AB}$ is an oscillatory integral whose phase parametrizes the image of the critical manifold under the map retaining the exterior covectors \begin{align*} (x,y,z,\theta,\sigma) \mapsto (x,\partial_x\phi_1(x,y,\theta);z,\partial_z\phi_2(y,z,\sigma)). \end{align*} Under the identification made in the previous step, this map is exactly $\pi_{XZ}$. The product amplitude $a=a_1a_2$ has the combined symbol order corresponding to $m_1+m_2$ in the chapter's kernel-order convention. By the explicit normalization hypothesis in the theorem statement, clean stationary phase along a clean critical manifold of excess $e$ shifts the resulting kernel order by \begin{align*} \frac{e}{2}. \end{align*} Hence the resulting kernel has order \begin{align*} m_1+m_2+\frac{e}{2}. \end{align*} This is the same rule as in the standard half-density operator-order convention after applying the chapter's stated translation between kernel order and operator order.[/step]

[guided]The stationary phase step has two separate hypotheses, and both must be checked at the level of the actual phase variables. First, the critical set of $\Phi$ with respect to $(y,\theta,\sigma)$ must be a smooth clean critical manifold. The theorem statement makes this explicit: for each microlocal phase representation, this critical set maps diffeomorphically onto the corresponding piece of \begin{align*} C_1 \times_{T^*Y}^{-} C_2. \end{align*} The equations defining that critical set are $\partial_\theta\phi_1=0$, $\partial_\sigma\phi_2=0$, and $\partial_y\phi_1+\partial_y\phi_2=0$. The first two equations place the two points on $C_1$ and $C_2$, and the last equation is precisely the negative matching condition $\eta+\eta'=0$. Second, clean stationary phase requires constant rank of the Hessian normal to the critical manifold. This is also now a hypothesis of the theorem statement: the normal Hessian of $\Phi$ in the variables $(y,\theta,\sigma)$ has constant rank equal to the number of integration variables minus the fibre dimension determined by the excess $e$. Therefore the clean stationary phase theorem applies to the regularized oscillatory integral defining $K_{AB}$. The theorem then replaces the integration in the normal directions by a new amplitude and leaves the clean critical directions as parameters. The exterior covectors of the resulting oscillatory integral are obtained from the derivatives of the combined phase in the non-integrated variables: \begin{align*} (x,y,z,\theta,\sigma) \mapsto (x,\partial_x\phi_1(x,y,\theta);z,\partial_z\phi_2(y,z,\sigma)). \end{align*} Because the critical set has already been identified with the negative fibre product, this map is exactly \begin{align*} \pi_{XZ}: C_1 \times_{T^*Y}^{-} C_2 \to (T^*X \setminus 0) \times (T^*Z \setminus 0). \end{align*} Thus the new oscillatory integral is associated with the projected canonical relation. Finally we track the order. The product amplitude $a=a_1a_2$ has the combined symbol order corresponding to $m_1+m_2$ in the chapter's kernel-order convention, because symbol orders add under multiplication. The theorem statement explicitly records the chapter normalization used by this composition theorem: clean stationary phase for a clean critical manifold with excess $e$ contributes the order shift \begin{align*} \frac{e}{2}. \end{align*} Therefore the composed kernel has order \begin{align*} m_1+m_2+\frac{e}{2}. \end{align*} This gives the same order formula after translating to the standard half-density operator-order convention.[/guided]

[step:Use properness and constant rank to identify the composed Lagrangian target] The theorem assumes that $\pi_{XZ}$ is proper and has constant rank on the closed conic subset of $C_1 \times_{T^*Y}^{-} C_2$ [lying over](/theorems/2944) $\operatorname{WF}'(A)\times\operatorname{WF}'(B)$. Properness ensures that the pushforward of the local oscillatory representation has no escaping contribution at infinity in the fibre-product variables. Constant rank ensures that the projected image is locally an immersed conic submanifold on the wavefront-relevant set. By the additional hypothesis in the statement, this image \begin{align*} C_1 \circ C_2=\pi_{XZ}(C_1 \times_{T^*Y}^{-} C_2) \end{align*} is an admissible immersed conic Lagrangian target for the class $I^m(X,Z;C_1\circ C_2)$. The local oscillatory integrals produced above are therefore precisely local representatives of an element of \begin{align*} I^{m_1+m_2+e/2}(X,Z;C_1\circ C_2). \end{align*} The microlocal pieces patch by the standard equivalence of phase parametrizations in the definition of Fourier integral distributions. Hence \begin{align*} AB \in I^{m_1+m_2+e/2}(X,Z;C_1\circ C_2). \end{align*} This proves the asserted composition statement in the chapter's kernel-order convention, and the final equivalence with the half-density operator-order convention follows from the same normalization translation used in the chapter's definition of the input classes. [/step]