[proofplan] We compare the same Schwartz kernel written in two coordinate systems. Under the coordinate change, the phase is rewritten by separating its diagonal linear part from a remainder vanishing to second order at the diagonal. The linear part gives exactly the cotangent transformation $\xi=(d\kappa_x)^*\eta$, while the second-order remainder enters the standard symbolic expansion only in lower order. For half-densities, the Jacobian factors coming from the change of coordinates cancel at the diagonal, so the leading symbol is transformed purely by the cotangent lift. [/proofplan]

[step:Write the kernel in the first coordinate system] Let $X := \varphi(U \cap V) \subset \mathbb{R}^n$ and $Y := \psi(U \cap V) \subset \mathbb{R}^n$. Let $\mathcal{L}^n$ denote Lebesgue measure on $\mathbb{R}^n$, and let $\mathcal{L}^1$ denote Lebesgue measure on $\mathbb{R}$. The coordinate transition map is the smooth diffeomorphism $\kappa: X \to Y$ defined by $\kappa(x) := \psi(\varphi^{-1}(x))$. Its inverse is the smooth diffeomorphism $\theta: Y \to X$ defined by $\theta(y) := \varphi(\psi^{-1}(y))$. After the half-density trivialization in the $x$-coordinates, define the scalar kernel representative $K_x: X \times X \times (0,h_0] \to \mathbb{C}$ by the semiclassical oscillatory integral \begin{align*} K_x(x,x';h) := (2\pi h)^{-n} \int_{\mathbb{R}^n} e^{i(x-x')\cdot \xi/h} a(x,\xi;h)\, d\mathcal{L}^n(\xi). \end{align*} The integral is interpreted in the standard oscillatory-integral sense, equivalently by inserting a compactly supported cutoff in $\xi$ and taking the cutoff limit in the distributional kernel topology. The kernel of $A_h$ near the diagonal is represented by $K_x$ modulo an $O(h^\infty)$ smoothing kernel. Here \begin{align*} a: X \times \mathbb{R}^n \times (0,h_0] \to \mathbb{C} \end{align*} is a full semiclassical symbol in $S^m$. By definition, the local principal symbol in the $x$-coordinates is the class \begin{align*} a_0 := a \mod hS^{m-1}. \end{align*} [/step]

[step:Transform the half-density kernel to the second coordinate system]Let $J_\theta: Y \to (0,\infty)$ be the smooth function defined by \begin{align*} J_\theta(y) := |\det d\theta_y|. \end{align*} This is the absolute Jacobian determinant of the inverse coordinate change. Define the scalar kernel representative in the $y$-coordinates as the map $K_y: Y \times Y \times (0,h_0] \to \mathbb{C}$. Because $A_h$ acts on half-densities, this map is given by \begin{align*} K_y(y,y';h) = J_\theta(y)^{1/2} J_\theta(y')^{1/2} K_x(\theta(y),\theta(y');h). \end{align*} Substituting the oscillatory representation of $K_x$ gives \begin{align*} K_y(y,y';h) = (2\pi h)^{-n} \int_{\mathbb{R}^n} e^{i(\theta(y)-\theta(y'))\cdot \xi/h} J_\theta(y)^{1/2} J_\theta(y')^{1/2} a(\theta(y),\xi;h)\, d\mathcal{L}^n(\xi) \end{align*} modulo an $O(h^\infty)$ smoothing kernel.[/step]

[guided]The only point in this step is to track the type of the object being transformed. The Schwartz kernel of an operator on half-densities is itself a half-density in both variables. Thus, when we rewrite the same kernel using the coordinates $y$ and $y'$, the scalar coefficient changes by one square-root Jacobian factor in each variable. We define the smooth function $J_\theta: Y \to (0,\infty)$ by \begin{align*} J_\theta(y) := |\det d\theta_y|. \end{align*} We also define $K_y: Y \times Y \times (0,h_0] \to \mathbb{C}$ to be the scalar representative of the transformed kernel in the $y$-coordinates. The half-density transformation rule gives \begin{align*} K_y(y,y';h) = J_\theta(y)^{1/2} J_\theta(y')^{1/2} K_x(\theta(y),\theta(y');h). \end{align*} Now substitute the $x$-coordinate oscillatory formula for $K_x$. Since \begin{align*} K_x(x,x';h) = (2\pi h)^{-n} \int_{\mathbb{R}^n} e^{i(x-x')\cdot \xi/h} a(x,\xi;h)\, d\mathcal{L}^n(\xi) \end{align*} near the diagonal, setting $x=\theta(y)$ and $x'=\theta(y')$ yields \begin{align*} K_y(y,y';h) = (2\pi h)^{-n} \int_{\mathbb{R}^n} e^{i(\theta(y)-\theta(y'))\cdot \xi/h} J_\theta(y)^{1/2} J_\theta(y')^{1/2} a(\theta(y),\xi;h)\, d\mathcal{L}^n(\xi). \end{align*} The $O(h^\infty)$ smoothing remainder remains of the same residual type under multiplication by smooth Jacobian factors and pullback by the diffeomorphism $\theta$.[/guided]

[step:Extract the linear part of the transformed phase] Fix $y \in Y$. For $y'$ sufficiently close to $y$, define the smooth matrix-valued map $B_y: Y \to \mathbb{R}^{n \times n}$ by \begin{align*} B_y(y') := \int_0^1 d\theta_{y' + t(y-y')} \, d\mathcal{L}^1(t). \end{align*} The fundamental theorem of calculus applied to the smooth map $t \mapsto \theta(y' + t(y-y'))$ gives \begin{align*} \theta(y)-\theta(y') = B_y(y') (y-y'). \end{align*} Then $B_y(y)=d\theta_y$, and $B_y(y')$ is invertible after restricting to a sufficiently small neighbourhood of the diagonal. With the change of fibre variable $\eta := B_y(y')^\top \xi$, equivalently $\xi = B_y(y')^{-\top}\eta$, the phase becomes \begin{align*} (\theta(y)-\theta(y'))\cdot \xi = (y-y')\cdot \eta. \end{align*} The Lebesgue measure transforms as \begin{align*} d\mathcal{L}^n(\xi) = |\det B_y(y')|^{-1}\, d\mathcal{L}^n(\eta). \end{align*} Therefore the transformed kernel can be written as \begin{align*} K_y(y,y';h) = (2\pi h)^{-n} \int_{\mathbb{R}^n} e^{i(y-y')\cdot \eta/h} c(y,y',\eta;h)\, d\mathcal{L}^n(\eta), \end{align*} where the amplitude $c: Y \times Y \times \mathbb{R}^n \times (0,h_0] \to \mathbb{C}$ is the map defined by \begin{align*} c(y,y',\eta;h) = J_\theta(y)^{1/2} J_\theta(y')^{1/2} |\det B_y(y')|^{-1} a\bigl(\theta(y),B_y(y')^{-\top}\eta;h\bigr). \end{align*} [/step]

[step:Restrict the amplitude to the diagonal to identify the principal term] The smoothness of $J_\theta$, the smoothness of $B_y(y')$, the local invertibility of $B_y(y')$ near the diagonal, and the symbol estimates for $a \in S^m$ imply that $c$ satisfies the local semiclassical amplitude estimates of order $m$ uniformly for $(y,y')$ in a sufficiently small neighbourhood of the diagonal. The kernel is localized near the diagonal and is properly supported in this coordinate patch, so the standard semiclassical amplitude-to-left-symbol theorem applies: a properly supported oscillatory kernel with amplitude in this local class has a left symbol obtained by the usual Taylor expansion in $y'-y$, with each correction containing one $h\partial_\eta$ factor. Define $\partial_{y'}^\alpha$ to be the ordinary multi-index partial derivative in the primed base variable. The resulting left symbol $\tilde b: Y \times \mathbb{R}^n \times (0,h_0] \to \mathbb{C}$ satisfies \begin{align*} \tilde b(y,\eta;h) \sim \sum_{|\alpha| \geq 0} \frac{h^{|\alpha|}}{i^{|\alpha|}\alpha!} \partial_\eta^\alpha \partial_{y'}^\alpha c(y,y',\eta;h)\big|_{y'=y}. \end{align*} The term with $\alpha=0$ is $c(y,y,\eta;h)$, and every term with $|\alpha| \geq 1$ lies in $hS^{m-1}$ because each $\eta$-derivative lowers the symbol order by one and the expansion supplies a factor of $h^{|\alpha|}$. Hence \begin{align*} \tilde b(y,\eta;h) = c(y,y,\eta;h) \mod hS^{m-1}. \end{align*} The assumed symbol $b$ in the $y$-chart represents the same local kernel modulo an $O(h^\infty)$ smoothing remainder. The uniqueness statement for local left symbols says that two left symbols producing the same properly supported semiclassical kernel modulo an $O(h^\infty)$ smoothing kernel have the same principal class modulo $hS^{m-1}$. Applying this uniqueness statement to $b$ and $\tilde b$ shows that $b$ and $\tilde b$ have the same class modulo $hS^{m-1}$. At $y'=y$, we have $B_y(y)=d\theta_y$ and \begin{align*} |\det B_y(y)| = |\det d\theta_y| = J_\theta(y) \end{align*} Thus the half-density Jacobian factor satisfies \begin{align*} J_\theta(y)^{1/2} J_\theta(y)^{1/2} |\det B_y(y)|^{-1} = J_\theta(y)J_\theta(y)^{-1} = 1 \end{align*} Consequently, \begin{align*} b(y,\eta;h) = a\bigl(\theta(y),(d\theta_y)^{-\top}\eta;h\bigr) \mod hS^{m-1}. \end{align*} Since $x=\theta(y)$ and $d\theta_y=(d\kappa_x)^{-1}$, the transpose inverse identity gives \begin{align*} (d\theta_y)^{-\top} = (d\kappa_x)^\top \end{align*} In covector notation, this is exactly \begin{align*} (d\theta_y)^{-\top}\eta = (d\kappa_x)^*\eta \end{align*} Passing to classes modulo $hS^{m-1}$ yields \begin{align*} b_0(y,\eta)=a_0\bigl(x,(d\kappa_x)^*\eta\bigr) \end{align*} [/step]

[step:Conclude that the principal symbol is globally defined] The preceding identity is precisely the compatibility condition for local representatives of a function on $T^*M$: if the same covector is written as $(x,\xi)$ in the first chart and as $(y,\eta)$ in the second chart, with \begin{align*} y=\kappa(x), \qquad \xi=(d\kappa_x)^*\eta \end{align*} then the two local principal symbols agree: \begin{align*} b_0(y,\eta)=a_0(x,\xi). \end{align*} Therefore the principal symbol representatives glue to a coordinate-independent class \begin{align*} \sigma_h^m(A_h) \in S^m(T^*M)/hS^{m-1}(T^*M) \end{align*} For operators acting on functions rather than half-densities, the same computation contains the Jacobian factors determined by the chosen density convention. Once that convention is fixed, the principal term still transforms by the cotangent lift, while the remaining density-dependent contributions enter the lower-order terms of the full symbol. This proves the stated coordinate invariance. [/step]