[proofplan]
We first compute the effect of $(hD_x)^\alpha$ on a WKB-type test function $e^{i\phi/h}b$ and show that its leading term is multiplication by $(\partial_x\phi)^\alpha$. This identifies the top homogeneous polynomial in the covector $d\phi_x$ as the sum of the order-$m$ terms with coefficients evaluated at $h=0$. Finally, we check coordinate invariance: covectors transform by the cotangent lift, and the tensorial transformation law for the top-order coefficients is precisely the statement that the resulting degree-$m$ polynomial has the same value in every chart.
[/proofplan]
[step:Compute the leading action of one semiclassical derivative on an oscillatory test function]
Let
\begin{align*}
\phi: U \to \mathbb{R}
\end{align*}
be a smooth real-valued function and let
\begin{align*}
b: U \to \mathbb{C}
\end{align*}
be a smooth amplitude. Define the oscillatory test function
\begin{align*}
u_h: U \to \mathbb{C}
\end{align*}
by
\begin{align*}
u_h(x)=e^{i\phi(x)/h}b(x).
\end{align*}
For each coordinate index $j \in \{1,\dots,n\}$, the definition $D_{x_j}=-i\partial_{x_j}$ gives
\begin{align*}
hD_{x_j}u_h
=
-i h \partial_{x_j}\left(e^{i\phi/h}b\right).
\end{align*}
Using the product rule and the chain rule,
\begin{align*}
\partial_{x_j}\left(e^{i\phi/h}b\right)
=
e^{i\phi/h}\left(\frac{i}{h}\partial_{x_j}\phi\right)b
+
e^{i\phi/h}\partial_{x_j}b.
\end{align*}
Therefore
\begin{align*}
hD_{x_j}u_h
=
e^{i\phi/h}(\partial_{x_j}\phi)b
-
ih e^{i\phi/h}\partial_{x_j}b.
\end{align*}
Equivalently,
\begin{align*}
e^{-i\phi/h}hD_{x_j}\left(e^{i\phi/h}b\right)
=
(\partial_{x_j}\phi)b
-
ih\partial_{x_j}b.
\end{align*}
Thus a single semiclassical derivative contributes multiplication by the corresponding covector component $\partial_{x_j}\phi$ at order $h^0$, while the derivative falling on $b$ carries an extra factor of $h$.
[guided]
We test the operator on an oscillatory function because the exponential records covectors. Let
\begin{align*}
\phi: U \to \mathbb{R}
\end{align*}
be smooth, let
\begin{align*}
b: U \to \mathbb{C}
\end{align*}
be smooth, and define
\begin{align*}
u_h: U \to \mathbb{C}
\end{align*}
by
\begin{align*}
u_h(x)=e^{i\phi(x)/h}b(x).
\end{align*}
The covector encoded by this oscillation at $x$ is $d\phi_x$, whose coordinate components are $\partial_{x_1}\phi(x),\dots,\partial_{x_n}\phi(x)$.
Fix $j \in \{1,\dots,n\}$. Since $D_{x_j}=-i\partial_{x_j}$, we compute directly:
\begin{align*}
hD_{x_j}u_h
=
-ih\partial_{x_j}\left(e^{i\phi/h}b\right).
\end{align*}
The product rule separates the derivative falling on the exponential from the derivative falling on the amplitude. The chain rule gives
\begin{align*}
\partial_{x_j}e^{i\phi/h}
=
e^{i\phi/h}\frac{i}{h}\partial_{x_j}\phi.
\end{align*}
Hence
\begin{align*}
\partial_{x_j}\left(e^{i\phi/h}b\right)
=
e^{i\phi/h}\left(\frac{i}{h}\partial_{x_j}\phi\right)b
+
e^{i\phi/h}\partial_{x_j}b.
\end{align*}
Multiplying by $-ih$ gives
\begin{align*}
hD_{x_j}u_h
=
e^{i\phi/h}(\partial_{x_j}\phi)b
-
ih e^{i\phi/h}\partial_{x_j}b.
\end{align*}
After removing the common oscillatory factor, this becomes
\begin{align*}
e^{-i\phi/h}hD_{x_j}\left(e^{i\phi/h}b\right)
=
(\partial_{x_j}\phi)b
-
ih\partial_{x_j}b.
\end{align*}
This calculation is the basic reason for the convention $D_{x_j}=-i\partial_{x_j}$: the leading term is exactly $\partial_{x_j}\phi$, with no additional factor of $i$. The second term is lower in the semiclassical expansion because it has an explicit factor of $h$.
[/guided]
[/step]
[step:Extend the computation to arbitrary multi-indices]
For a multi-index $\alpha \in \mathbb{N}_0^n$, define the smooth remainder
\begin{align*}
r_{\alpha,h}: U \to \mathbb{C}
\end{align*}
by the identity
\begin{align*}
e^{-i\phi/h}(hD_x)^\alpha(e^{i\phi/h}b)
=
(\partial_x\phi)^\alpha b
+
h r_{\alpha,h}.
\end{align*}
We prove that such an $r_{\alpha,h}$ exists by induction on $|\alpha|$.
For $|\alpha|=0$, the identity holds with $r_{0,h}=0$. Suppose it holds for $\alpha$, and let $e_j \in \mathbb{N}_0^n$ denote the multi-index with $1$ in the $j$-th component and $0$ elsewhere. Then
\begin{align*}
(hD_x)^{\alpha+e_j}(e^{i\phi/h}b)
=
hD_{x_j}\left(e^{i\phi/h}\left((\partial_x\phi)^\alpha b+h r_{\alpha,h}\right)\right).
\end{align*}
Applying the single-derivative computation with amplitude $(\partial_x\phi)^\alpha b+h r_{\alpha,h}$ gives
\begin{align*}
e^{-i\phi/h}(hD_x)^{\alpha+e_j}(e^{i\phi/h}b)
=
(\partial_{x_j}\phi)\left((\partial_x\phi)^\alpha b+h r_{\alpha,h}\right)
-
ih\partial_{x_j}\left((\partial_x\phi)^\alpha b+h r_{\alpha,h}\right).
\end{align*}
The first term of order $h^0$ is $(\partial_x\phi)^{\alpha+e_j}b$. All remaining terms contain a factor of $h$, so they define a smooth remainder $r_{\alpha+e_j,h}$. This proves the asserted expansion for every multi-index $\alpha$.
[/step]
[step:Extract the homogeneous degree-$m$ polynomial from the oscillatory test]
Applying $P_h$ to $u_h=e^{i\phi/h}b$ and using the multi-index expansion gives
\begin{align*}
e^{-i\phi/h}P_h(e^{i\phi/h}b)
=
\sum_{|\alpha|\leq m} a_\alpha(x;h)(\partial_x\phi)^\alpha b
+
h\sum_{|\alpha|\leq m} a_\alpha(x;h)r_{\alpha,h}.
\end{align*}
Since each coefficient $a_\alpha(x;h)$ is continuous at $h=0$, the order-$h^0$ coefficient tends, as $h \to 0$, to
\begin{align*}
\sum_{|\alpha|\leq m} a_\alpha(x;0)(\partial_x\phi)^\alpha b.
\end{align*}
The part homogeneous of degree $m$ in the covector $\partial_x\phi(x)$ is exactly
\begin{align*}
\sum_{|\alpha|=m} a_\alpha(x;0)(\partial_x\phi(x))^\alpha b(x).
\end{align*}
Because the covector $d\phi_x \in T_x^*U$ has coordinate representation $\partial_x\phi(x) \in \mathbb{R}^n$, the degree-$m$ multiplier is the polynomial
\begin{align*}
p_m(x,\xi)=\sum_{|\alpha|=m} a_\alpha(x;0)\xi^\alpha.
\end{align*}
This proves the local formula for the semiclassical principal symbol.
[/step]
[step:Show that the top-order expression transforms as a function on the cotangent bundle]
Let $(U,x)$ and $(V,y)$ be two coordinate charts on a smooth manifold $M$ with $U \cap V \neq \varnothing$. Write $x=(x_1,\dots,x_n)$ and $y=(y_1,\dots,y_n)$. Let
\begin{align*}
\kappa: y(U\cap V) \to x(U\cap V)
\end{align*}
be the coordinate change map defined by $\kappa(y(q))=x(q)$ for $q \in U\cap V$.
At a point $q \in U\cap V$, a covector $\zeta \in T_q^*M$ has coordinate components $\xi \in \mathbb{R}^n$ in the $x$-chart and $\eta \in \mathbb{R}^n$ in the $y$-chart related by the cotangent transformation law
\begin{align*}
\eta_j
=
\sum_{k=1}^n \frac{\partial x_k}{\partial y_j}(y(q))\xi_k.
\end{align*}
Equivalently, $\eta$ is the pullback of $\xi$ by the differential of the coordinate change.
By hypothesis, the top-order coefficients of the globally defined operator determine a symmetric contravariant $m$-tensor at $h=0$. Denote this tensor by
\begin{align*}
A_m(q): (T_q^*M)^m \to \mathbb{C}.
\end{align*}
In the $x$-chart, its contraction against $\zeta$ repeated $m$ times is
\begin{align*}
A_m(q)(\zeta,\dots,\zeta)
=
\sum_{|\alpha|=m} a_\alpha^x(x(q);0)\xi^\alpha.
\end{align*}
In the $y$-chart, the same tensor contraction is
\begin{align*}
A_m(q)(\zeta,\dots,\zeta)
=
\sum_{|\alpha|=m} a_\alpha^y(y(q);0)\eta^\alpha.
\end{align*}
The equality of these two expressions is precisely the tensorial transformation law for the top-order coefficients. Therefore the local formula defines the same complex number for every coordinate representation of the covector $\zeta$.
[/step]
[step:Conclude the global well-definedness of the principal symbol]
Define
\begin{align*}
p_m: T^*M \to \mathbb{C}
\end{align*}
by
\begin{align*}
p_m(q,\zeta)=A_m(q)(\zeta,\dots,\zeta).
\end{align*}
The previous step shows that, in every coordinate chart, this function is represented by
\begin{align*}
p_m(x,\xi)=\sum_{|\alpha|=m} a_\alpha(x;0)\xi^\alpha.
\end{align*}
Since tensor contraction is coordinate-independent and the local coefficients are smooth in the base variable, $p_m$ is a globally well-defined smooth function on $T^*M$. This proves both the local formula and the asserted coordinate-invariant global interpretation of the semiclassical principal symbol.
[/step]
