Let $n \in \mathbb{N}$, let $h_0>0$, let $m: T^*\mathbb{R}^n \to (0,\infty)$ be an order function, and let $S(m)$ denote the corresponding semiclassical symbol class on $T^*\mathbb{R}^n$. Let $\#$ denote the semiclassical Weyl product on these symbol classes, and let $\operatorname{Op}_h^w$ denote semiclassical Weyl quantization on Schwartz functions. Let $a: T^*\mathbb{R}^n \to \mathbb{R}$ be a real-valued symbol with $a \in S(m)$. Assume that there exists a constant $c>0$ such that

\begin{align*} a(x,\xi) \geq c\,m(x,\xi) \end{align*}

for every $(x,\xi) \in T^*\mathbb{R}^n$. Then there exists a real-valued $h$-dependent symbol family $b_h: T^*\mathbb{R}^n \to \mathbb{R}$, defined for $0<h\leq h_0$, such that $b_h$ is bounded uniformly in $S(m^{1/2})$ and

\begin{align*} b_h \# b_h - a \in h^2 S(m). \end{align*}

Equivalently, there exists a family $r_h: T^*\mathbb{R}^n \to \mathbb{C}$ bounded uniformly in $S(m)$ for $0<h\leq h_0$ such that

\begin{align*} b_h \# b_h = a + h^2 r_h. \end{align*}

Consequently, as an identity of operators on Schwartz functions, with $*$ denoting the formal adjoint on Schwartz functions,

\begin{align*} (\operatorname{Op}_h^w(b_h))^* \operatorname{Op}_h^w(b_h) = \operatorname{Op}_h^w(a) + h^2 \operatorname{Op}_h^w(r_h), \end{align*}

where $r_h$ is bounded uniformly in $S(m)$ for $0<h\leq h_0$.