[proofplan]
We compute the commutator at the level of Weyl symbols. The Weyl product admits the Moyal expansion, whose first terms are the ordinary product, the Poisson bracket term, and higher bidifferential corrections. Exchanging the two symbols changes the sign of the odd Moyal terms and preserves the even Moyal terms, so the zeroth and all even powers cancel in the commutator. The first surviving term is $\frac{h}{i}\{a,b\}$, and the next surviving term is cubic in $h$, with symbol order lowered by three and with all symbol estimates uniform for $h \in (0,h_0]$. The non-Weyl comparison follows from the same symbolic composition principle, but without the midpoint symmetry that cancels the second-order commutator contribution.
[/proofplan]
[step:Write the commutator symbol using the Weyl product]
Let $c=(c_h)_{0<h\leq h_0}$ denote the semiclassical Weyl symbol family of the product $\operatorname{Op}_h^w(a_h)\operatorname{Op}_h^w(b_h)$, with each component $c_h: T^*\mathbb{R}^n \to \mathbb{C}$. The semiclassical Weyl composition theorem gives
\begin{align*}
\operatorname{Op}_h^w(a_h)\operatorname{Op}_h^w(b_h) = \operatorname{Op}_h^w(c_h)
\end{align*}
modulo residual semiclassical operators, uniformly for $0<h\leq h_0$. By definition of the Weyl product, we write $c_h = a_h \#_w b_h$. Similarly,
\begin{align*}
\operatorname{Op}_h^w(b_h)\operatorname{Op}_h^w(a_h) = \operatorname{Op}_h^w(b_h \#_w a_h)
\end{align*}
modulo residual semiclassical operators. Therefore the Weyl symbol of the commutator is
\begin{align*}
a_h \#_w b_h - b_h \#_w a_h.
\end{align*}
[/step]
[step:Expand the two Weyl products by the Moyal formula]
For smooth functions $A,B: T^*\mathbb{R}^n \to \mathbb{C}$, define the bilinear first-order differential operator $\Lambda$ by
\begin{align*}
\Lambda(A,B)(x,\xi) = \sum_{j=1}^n \partial_{\xi_j}A(x,\xi)\,\partial_{x_j}B(x,\xi) - \partial_{x_j}A(x,\xi)\,\partial_{\xi_j}B(x,\xi).
\end{align*}
Thus $\Lambda(a,b)=\{a,b\}$. For each $k \in \mathbb{N}$, define $\Lambda_k(A,B): T^*\mathbb{R}^n \to \mathbb{C}$ to be the $k$-fold iterated constant-coefficient symplectic bidifferential operator obtained from $\Lambda$, with $\Lambda_0(A,B):=AB$ and $\Lambda_1(A,B):=\Lambda(A,B)$. Thus $\Lambda_k$ is the coefficient before the factor $t^k/k!$ in the Taylor expansion of $\exp(t\Lambda)(A,B)$. In particular,
\begin{align*}
\Lambda_0(a_h,b_h)=a_hb_h
\end{align*}
and
\begin{align*}
\Lambda_1(a_h,b_h)=\{a_h,b_h\}.
\end{align*}
We use the following semiclassical Weyl symbolic composition theorem. If $p=(p_h)_{0<h\leq h_0}\in S^\mu(T^*\mathbb{R}^n)$ and $q=(q_h)_{0<h\leq h_0}\in S^\nu(T^*\mathbb{R}^n)$, then $p_h\#_w q_h$ has the stopped Moyal expansion
\begin{align*}
p_h\#_w q_h=\sum_{k=0}^{N-1}\frac{1}{k!}\left(\frac{h}{2i}\right)^k\Lambda_k(p_h,q_h)+h^N e_{N,h}
\end{align*}
modulo residual semiclassical symbols, where $e_N=(e_{N,h})_{0<h\leq h_0}\in S^{\mu+\nu-N}(T^*\mathbb{R}^n)$ and all defining seminorm estimates are uniform for $0<h\leq h_0$. The hypotheses of this theorem are satisfied with $p=a$, $q=b$, $\mu=m$, $\nu=m'$, and $N=3$, because $a\in S^m(T^*\mathbb{R}^n)$ and $b\in S^{m'}(T^*\mathbb{R}^n)$ are semiclassical symbol families on the common phase space $T^*\mathbb{R}^n$. Therefore there exists a family $q_3(a,b)=(q_{3,h}(a,b))_{0<h\leq h_0}\in S^{m+m'-3}(T^*\mathbb{R}^n)$ such that
\begin{align*}
a_h \#_w b_h = a_hb_h + \frac{h}{2i}\{a_h,b_h\} + \frac{1}{2}\left(\frac{h}{2i}\right)^2\Lambda_2(a_h,b_h) + h^3 q_{3,h}(a,b).
\end{align*}
Applying the same theorem with the two factors exchanged gives a family $q_3(b,a)=(q_{3,h}(b,a))_{0<h\leq h_0}\in S^{m+m'-3}(T^*\mathbb{R}^n)$ such that
\begin{align*}
b_h \#_w a_h = b_ha_h + \frac{h}{2i}\{b_h,a_h\} + \frac{1}{2}\left(\frac{h}{2i}\right)^2\Lambda_2(b_h,a_h) + h^3 q_{3,h}(b,a).
\end{align*}
[guided]
The goal is to convert the operator commutator into a symbol computation with every $h$-dependent object visible. For Weyl quantization, the semiclassical Weyl symbolic composition theorem says that if $p\in S^\mu(T^*\mathbb{R}^n)$ and $q\in S^\nu(T^*\mathbb{R}^n)$, then $\operatorname{Op}_h^w(p_h)\operatorname{Op}_h^w(q_h)$ is represented, modulo residual semiclassical operators, by $\operatorname{Op}_h^w(p_h\#_w q_h)$. It also gives the stopped Moyal expansion
\begin{align*}
p_h\#_w q_h=\sum_{k=0}^{N-1}\frac{1}{k!}\left(\frac{h}{2i}\right)^k\Lambda_k(p_h,q_h)+h^N e_{N,h},
\end{align*}
where $e_N=(e_{N,h})_{0<h\leq h_0}\in S^{\mu+\nu-N}(T^*\mathbb{R}^n)$ and all symbol seminorm estimates are uniform for $0<h\leq h_0$. The hypotheses are satisfied here with $p=a$, $q=b$, $\mu=m$, $\nu=m'$, and $N=3$, because $a\in S^m(T^*\mathbb{R}^n)$ and $b\in S^{m'}(T^*\mathbb{R}^n)$ are semiclassical symbol families on the same phase space.
Define the bilinear first-order differential operator $\Lambda$ on smooth functions $A,B: T^*\mathbb{R}^n \to \mathbb{C}$ by
\begin{align*}
\Lambda(A,B)(x,\xi) = \sum_{j=1}^n \partial_{\xi_j}A(x,\xi)\,\partial_{x_j}B(x,\xi) - \partial_{x_j}A(x,\xi)\,\partial_{\xi_j}B(x,\xi).
\end{align*}
For $k\in\mathbb{N}$, let $\Lambda_k(A,B)$ be the $k$-fold iterated constant-coefficient symplectic bidifferential operator obtained from $\Lambda$, with $\Lambda_0(A,B):=AB$ and $\Lambda_1(A,B):=\Lambda(A,B)$. Thus the factor $1/k!$ is written separately in the Moyal expansion. With the Poisson bracket convention in the theorem statement,
\begin{align*}
\Lambda_1(a_h,b_h)=\{a_h,b_h\}.
\end{align*}
Applying the stopped expansion to $a_h\#_w b_h$ gives a family $q_3(a,b)=(q_{3,h}(a,b))_{0<h\leq h_0}\in S^{m+m'-3}(T^*\mathbb{R}^n)$ such that
\begin{align*}
a_h \#_w b_h = a_hb_h + \frac{h}{2i}\{a_h,b_h\} + \frac{1}{2}\left(\frac{h}{2i}\right)^2\Lambda_2(a_h,b_h) + h^3 q_{3,h}(a,b).
\end{align*}
The same theorem applies after exchanging the factors, since $b\in S^{m'}(T^*\mathbb{R}^n)$ and $a\in S^m(T^*\mathbb{R}^n)$. Hence there is a family $q_3(b,a)=(q_{3,h}(b,a))_{0<h\leq h_0}\in S^{m+m'-3}(T^*\mathbb{R}^n)$ such that
\begin{align*}
b_h \#_w a_h = b_ha_h + \frac{h}{2i}\{b_h,a_h\} + \frac{1}{2}\left(\frac{h}{2i}\right)^2\Lambda_2(b_h,a_h) + h^3 q_{3,h}(b,a).
\end{align*}
Now subtract the second identity from the first. Scalar multiplication is commutative, so $a_hb_h-b_ha_h=0$. The Poisson bracket is antisymmetric, hence $\{b_h,a_h\}=-\{a_h,b_h\}$, and therefore
\begin{align*}
\frac{h}{2i}\{a_h,b_h\}-\frac{h}{2i}\{b_h,a_h\}=\frac{h}{i}\{a_h,b_h\}.
\end{align*}
The second Moyal coefficient is symmetric under exchanging the two arguments in the Weyl calculus, so $\Lambda_2(a_h,b_h)=\Lambda_2(b_h,a_h)$ and the second-order terms cancel.
Define the family $r_3=(r_{3,h})_{0<h\leq h_0}$ by
\begin{align*}
r_{3,h}=q_{3,h}(a,b)-q_{3,h}(b,a).
\end{align*}
Because $S^{m+m'-3}(T^*\mathbb{R}^n)$ is a vector space and the two remainder families have uniform seminorm estimates, $r_3\in S^{m+m'-3}(T^*\mathbb{R}^n)$. Therefore
\begin{align*}
a_h\#_w b_h-b_h\#_w a_h=\frac{h}{i}\{a_h,b_h\}+h^3r_{3,h}.
\end{align*}
Applying Weyl quantization to this symbol identity gives
\begin{align*}
[\operatorname{Op}_h^w(a_h),\operatorname{Op}_h^w(b_h)] = \frac{h}{i}\operatorname{Op}_h^w(\{a_h,b_h\}) + h^3\operatorname{Op}_h^w(r_{3,h})
\end{align*}
modulo residual semiclassical operators.
For a fixed non-Weyl semiclassical quantization $\operatorname{Op}_h^\kappa$ satisfying the standard symbolic composition formula, the first antisymmetric part of the composition coefficient is still the Poisson bracket. Hence the principal commutator term is again $\frac{h}{i}\operatorname{Op}_h^\kappa(\{a_h,b_h\})$. What changes is the second-order coefficient: without Weyl midpoint symmetry, the degree-two terms in the two products need not agree after exchanging the factors. Therefore the remaining second-order contribution is recorded as $h^2R_h$ with $R_h \in \Psi_h^{m+m'-2}(\mathbb{R}^n)$, modulo residual semiclassical operators, unless an extra symmetry forces that coefficient to cancel.
[/guided]
[/step]
[step:Cancel the even Moyal terms and identify the first-order term]
Since multiplication of scalar symbols is commutative, $a_hb_h-b_ha_h=0$. The Poisson bracket is antisymmetric, so
\begin{align*}
\{b_h,a_h\} = -\{a_h,b_h\}.
\end{align*}
Therefore
\begin{align*}
\frac{h}{2i}\{a_h,b_h\} - \frac{h}{2i}\{b_h,a_h\} = \frac{h}{i}\{a_h,b_h\}.
\end{align*}
The second Moyal coefficient is symmetric under exchanging the two symbols:
\begin{align*}
\Lambda_2(a_h,b_h)=\Lambda_2(b_h,a_h).
\end{align*}
Hence the second-order terms cancel in $a_h \#_w b_h - b_h \#_w a_h$.
[/step]
[step:Collect the cubic remainder as a symbol of order $m+m'-3$]
Define the family $r_3=(r_{3,h})_{0<h\leq h_0}$ by
\begin{align*}
r_{3,h} = q_{3,h}(a,b)-q_{3,h}(b,a).
\end{align*}
Since $q_3(a,b)$ and $q_3(b,a)$ both belong to $S^{m+m'-3}(T^*\mathbb{R}^n)$ with seminorms uniform for $0<h\leq h_0$, and $S^{m+m'-3}(T^*\mathbb{R}^n)$ is a vector space, we have
\begin{align*}
r_3 \in S^{m+m'-3}(T^*\mathbb{R}^n).
\end{align*}
Combining the preceding cancellations gives
\begin{align*}
a_h \#_w b_h - b_h \#_w a_h = \frac{h}{i}\{a_h,b_h\} + h^3 r_{3,h}.
\end{align*}
Applying Weyl quantization to this symbol identity yields
\begin{align*}
[\operatorname{Op}_h^w(a_h),\operatorname{Op}_h^w(b_h)] = \frac{h}{i}\operatorname{Op}_h^w(\{a_h,b_h\}) + h^3\operatorname{Op}_h^w(r_{3,h})
\end{align*}
modulo residual semiclassical operators.
[/step]
[step:Compare with non-Weyl quantizations]
For a fixed non-Weyl semiclassical quantization $\operatorname{Op}_h^\kappa$ satisfying the standard symbolic composition formula, the symbolic composition formula still has first commutator term $\frac{h}{i}\{a_h,b_h\}$, because the antisymmetric part of the first-order composition coefficient is the Poisson bracket. However, the second-order composition coefficients need not be symmetric under exchanging the two factors. Consequently the second-order terms generally do not cancel, and the natural remainder class is
\begin{align*}
h^2\Psi_h^{m+m'-2}.
\end{align*}
In Weyl quantization, the midpoint symmetry of the quantization is exactly what removes the even Moyal terms from the commutator, improving the remainder to cubic order.
[/step]
