[proofplan] The proof is local on the manifold, except for proper support. First we use local finiteness and the stated kernel-support hypothesis to show that the displayed sum defines a properly supported continuous operator. Then we test the operator between compactly supported cutoffs inside a single coordinate chart and reduce the resulting finite sum to ordinary semiclassical operators on an open subset of $\mathbb{R}^n$. The coordinate invariance and composition formulae show that each neighbouring chart contribution has the expected leading symbol, and the overlap compatibility of the local principal symbols makes those leading terms glue to the claimed global principal symbol. [/proofplan] [step:Construct the operator from a locally finite sum of kernels] For each $j\in J$, define the local summand \begin{align*} A_{j,h}: C_c^\infty(M) &\to C^\infty(M) \end{align*} by \begin{align*} A_{j,h}u := \chi_j\,\operatorname{Op}_{h,\kappa_j}(a_j)(\psi_j u), \end{align*} where $u\in C_c^\infty(M)$ and $\psi_j u$ is regarded as a compactly supported function on $U_j$ before applying the chart quantization. Let $K_{j,h}\in \mathcal{D}'(M\times M)$ denote the Schwartz kernel of $A_{j,h}$. Since $\chi_j,\psi_j\in C_c^\infty(U_j)$, the support of $K_{j,h}$ is contained in \begin{align*} \operatorname{supp}\chi_j \times \operatorname{supp}\psi_j. \end{align*} The family $\{U_j\}_{j\in J}$ is locally finite, and the hypotheses explicitly require that, for each compact set $K\subset M$, only finitely many summand kernels meet $K\times M$ and only finitely many meet $M\times K$. Hence the distributional sum \begin{align*} K_h := \sum_{j\in J} K_{j,h} \end{align*} is locally finite on $M\times M$ and therefore defines a distribution in $\mathcal{D}'(M\times M)$. Let \begin{align*} A_h:C_c^\infty(M)&\to \mathcal{D}'(M) \end{align*} be the operator with Schwartz kernel $K_h$. For every compactly supported input $u\in C_c^\infty(M)$ and every compactly supported test density in the output variable, the pairing with $K_h$ contains only finitely many summands. Thus $A_h$ is precisely the locally finite sum \begin{align*} A_hu = \sum_{j\in J} A_{j,h}u \end{align*} in the sense of distributions. Since each $A_{j,h}$ is a local semiclassical pseudodifferential operator followed and preceded by compactly supported smooth multiplication, each finite localized sum maps $C_c^\infty$ continuously to $C^\infty$. [/step] [step:Verify proper support from the kernel hypothesis] Let \begin{align*} \pi_L:M\times M&\to M \end{align*} and \begin{align*} \pi_R:M\times M&\to M \end{align*} denote the left and right projections. The hypothesis says exactly that for every compact set $K\subset M$, the intersections \begin{align*} \operatorname{supp}K_h\cap (K\times M) \end{align*} and \begin{align*} \operatorname{supp}K_h\cap (M\times K) \end{align*} are obtained from finitely many summand kernels and have compact projections under $\pi_R$ and $\pi_L$, respectively. Therefore $\pi_L$ and $\pi_R$ restrict to proper maps on $\operatorname{supp}K_h$. This is the definition of proper support for the Schwartz kernel of an operator on $M$, so $A_h$ is properly supported. [/step] [step:Localize the operator to a single chart and reduce to finitely many neighbouring summands] Fix a point $x_0\in M$. Choose an index $\ell\in J$ with $x_0\in U_\ell$. Choose functions \begin{align*} \theta_0,\theta_1\in C_c^\infty(U_\ell) \end{align*} such that $\theta_1=1$ on an open neighbourhood of $\operatorname{supp}\theta_0$. It is enough to show that \begin{align*} \theta_0 A_h\theta_1 \end{align*} is, in the chart $\kappa_\ell$, a semiclassical pseudodifferential operator of order $m$ modulo a residual smoothing operator, with the asserted principal symbol on $T^*U_\ell$. Because the cover and the cutoffs are locally finite, only finitely many indices $k\in J$ satisfy \begin{align*} \operatorname{supp}\theta_0 \cap \operatorname{supp}\chi_k \neq \varnothing \end{align*} or \begin{align*} \operatorname{supp}\theta_1 \cap \operatorname{supp}\psi_k \neq \varnothing. \end{align*} Consequently \begin{align*} \theta_0 A_h\theta_1 = \sum_{k\in F} \theta_0\chi_k\,\operatorname{Op}_{h,\kappa_k}(a_k)\,\psi_k\theta_1 \end{align*} for a finite set $F\subset J$, modulo summands whose left and right cutoffs have separated supports. Those separated-support summands are residual smoothing by the standard separated-support smoothing theorem for semiclassical pseudodifferential kernels (citing a result not yet in the wiki: separated support gives $h^\infty\Psi_h^{-\infty}$). Thus the localized operator is a finite sum of local chart contributions plus a residual smoothing term. [/step] [step:Rewrite neighbouring chart contributions in the fixed cotangent coordinates] For each $k\in F$, let \begin{align*} \Phi_{k\ell}: \kappa_\ell(U_k\cap U_\ell)&\to \kappa_k(U_k\cap U_\ell) \end{align*} be the coordinate transition map \begin{align*} \Phi_{k\ell} := \kappa_k\circ \kappa_\ell^{-1}. \end{align*} Its cotangent lift is the smooth map \begin{align*} T^*\Phi_{k\ell}:T^*\kappa_k(U_k\cap U_\ell)&\to T^*\kappa_\ell(U_k\cap U_\ell). \end{align*} By the semiclassical coordinate invariance theorem for pseudodifferential operators (citing a result not yet in the wiki: semiclassical coordinate invariance under diffeomorphisms), the operator \begin{align*} \theta_0\chi_k\,\operatorname{Op}_{h,\kappa_k}(a_k)\,\psi_k\theta_1 \end{align*} can be written in the fixed chart $\kappa_\ell$ as \begin{align*} \operatorname{Op}_{h,\kappa_\ell}(b_{k\ell}) + R_{k\ell,h}, \end{align*} where $b_{k\ell}\in S_h^m(T^*U_\ell)$ and $R_{k\ell,h}\in h^\infty\Psi_h^{-\infty}(U_\ell)$. Its principal symbol class is \begin{align*} b_{k\ell}\bmod hS_h^{m-1} = \theta_0\chi_k\psi_k\theta_1\, \sigma_k \end{align*} after transporting $\sigma_k$ to $T^*U_\ell$ by the cotangent coordinate change. The finite sum \begin{align*} b_\ell := \sum_{k\in F} b_{k\ell} \end{align*} belongs to $S_h^m(T^*U_\ell)$, because $F$ is finite and each $b_{k\ell}$ satisfies the local symbol estimates. Therefore \begin{align*} \theta_0 A_h\theta_1 = \operatorname{Op}_{h,\kappa_\ell}(b_\ell)+R_{\ell,h} \end{align*} with $R_{\ell,h}\in h^\infty\Psi_h^{-\infty}(U_\ell)$. [guided] We now explain why all neighbouring summands can be compared inside one cotangent coordinate system. The issue is that the $k$-th summand is quantized in the chart $\kappa_k$, while we want to prove that the total operator is pseudodifferential in the chart $\kappa_\ell$ near $x_0$. The comparison map is the coordinate transition \begin{align*} \Phi_{k\ell}: \kappa_\ell(U_k\cap U_\ell)&\to \kappa_k(U_k\cap U_\ell), \end{align*} defined by \begin{align*} \Phi_{k\ell} := \kappa_k\circ \kappa_\ell^{-1}. \end{align*} On cotangent variables, symbols transform by the cotangent lift \begin{align*} T^*\Phi_{k\ell}:T^*\kappa_k(U_k\cap U_\ell)&\to T^*\kappa_\ell(U_k\cap U_\ell). \end{align*} For a fixed $k\in F$, consider the localized operator \begin{align*} \theta_0\chi_k\,\operatorname{Op}_{h,\kappa_k}(a_k)\,\psi_k\theta_1. \end{align*} All four cutoffs are compactly supported in the region where the coordinate comparison is being made, after discarding separated-support terms. The semiclassical coordinate invariance theorem says that conjugating a local semiclassical pseudodifferential operator by a smooth coordinate change gives another semiclassical pseudodifferential operator of the same order, and that the principal symbol transforms by the cotangent lift of the coordinate change. Applying this theorem to the transition map $\Phi_{k\ell}$ gives a symbol $b_{k\ell}\in S_h^m(T^*U_\ell)$ and a residual smoothing operator $R_{k\ell,h}\in h^\infty\Psi_h^{-\infty}(U_\ell)$ such that \begin{align*} \theta_0\chi_k\,\operatorname{Op}_{h,\kappa_k}(a_k)\,\psi_k\theta_1 = \operatorname{Op}_{h,\kappa_\ell}(b_{k\ell})+R_{k\ell,h}. \end{align*} The leading symbol of multiplication by smooth cutoffs is multiplication by those cutoff functions, and derivatives of the cutoffs enter only in lower symbolic terms through the semiclassical composition formula (citing a result not yet in the wiki: semiclassical composition formula). Hence the principal symbol class of $b_{k\ell}$ is \begin{align*} b_{k\ell}\bmod hS_h^{m-1} = \theta_0\chi_k\psi_k\theta_1\,\sigma_k, \end{align*} where $\sigma_k$ has been transported to $T^*U_\ell$ by the cotangent coordinate change. The set $F$ is finite, so adding the symbols gives another order-$m$ symbol \begin{align*} b_\ell := \sum_{k\in F} b_{k\ell}. \end{align*} Adding the residual remainders still gives a residual remainder, and therefore \begin{align*} \theta_0 A_h\theta_1 = \operatorname{Op}_{h,\kappa_\ell}(b_\ell)+R_{\ell,h} \end{align*} for some $R_{\ell,h}\in h^\infty\Psi_h^{-\infty}(U_\ell)$. This proves the local pseudodifferential form of the operator near $x_0$. [/guided] [/step] [step:Compute the principal symbol and identify the glued class] Let \begin{align*} \sigma\in S_h^m(T^*M)/hS_h^{m-1}(T^*M) \end{align*} denote the class obtained by gluing the compatible local classes $\sigma_j$. This class is well-defined because the hypothesis says that $\sigma_j$ and $\sigma_k$ agree on each overlap $T^*(U_j\cap U_k)$ after the cotangent coordinate transition. On $T^*U_\ell$, the previous step gives \begin{align*} b_\ell \bmod hS_h^{m-1} = \sum_{k\in F} \theta_0\chi_k\psi_k\theta_1\,\sigma_k. \end{align*} On the region where $\theta_0$ is supported and $\theta_1=1$, we have $\psi_k=1$ wherever $\chi_k\neq 0$, because $\psi_k=1$ on an open neighbourhood of $\operatorname{supp}\chi_k$. Therefore, on this region, \begin{align*} \sum_{k\in F} \theta_0\chi_k\psi_k\theta_1\,\sigma_k = \theta_0 \sum_{k\in F}\chi_k\,\sigma. \end{align*} The partition of unity satisfies \begin{align*} \sum_{k\in J}\chi_k = 1 \end{align*} on $M$, and only the finitely many indices in $F$ contribute near $\operatorname{supp}\theta_0$. Hence \begin{align*} \theta_0 \sum_{k\in F}\chi_k\,\sigma = \theta_0\sigma. \end{align*} Thus the principal symbol of $\theta_0A_h\theta_1$ in the chart $\kappa_\ell$ is the restriction of $\sigma$ to $T^*U_\ell$. Since $x_0\in M$ was arbitrary, the operator $A_h$ is locally a semiclassical pseudodifferential operator of order $m$ in every coordinate chart, and its local principal symbols are the restrictions of the global glued class $\sigma$. Together with proper support proved above, this gives \begin{align*} A_h\in \Psi_h^m(M) \end{align*} and \begin{align*} \sigma(A_h)=\sigma. \end{align*} This is exactly the asserted globalization statement. [/step]