[proofplan] We prove the equivalence in the two directions. Starting from the operator definition, an elliptic annihilator near $(x_0,\xi_0)$ admits a semiclassical parametrix; after shrinking the spatial and frequency neighbourhoods, this expresses the localized distribution $\chi u_h$ microlocally over $V$ as a pseudodifferential image of an $O(h^\infty)$ family plus a residual term, hence its semiclassical Fourier transform is rapidly small. Conversely, the Fourier decay assumption allows us to choose a compactly supported symbol elliptic at $(x_0,\xi_0)$ and supported in the frequency region where the Fourier transform is rapidly small. The resulting operator kills $\chi u_h$ by direct Fourier inversion, while its action on $(1-\chi)u_h$ is residual because the spatial supports are separated. [/proofplan]

[step:Pass from an elliptic annihilator to microlocal Fourier decay]Assume first that $(x_0,\xi_0)\notin \operatorname{WF}_h(u_h)$ in the operator-theoretic sense. By definition, there exist a symbol $a\in C_c^\infty(T^*U)$ elliptic at $(x_0,\xi_0)$ and the corresponding semiclassical operator $A_h=\operatorname{Op}_h(a)$ such that \begin{align*} A_h u_h = O(h^\infty) \end{align*} in $C^\infty_{\mathrm{loc}}(U)$. Choose open sets $U_1\Subset U$ and $V\subset\mathbb{R}^n$ with $x_0\in U_1$ and $\xi_0\in V$ such that $a$ is elliptic on $U_1\times V$. Choose $\chi:U\to\mathbb{R}$ with $\chi\in C_c^\infty(U_1)$ and $\chi(x_0)\neq 0$. Choose an open neighbourhood $V_0\Subset V$ of $\xi_0$. We use the semiclassical elliptic parametrix theorem and composition calculus in the following precise form. Because $a$ is elliptic on a neighbourhood of $\operatorname{supp}\chi\times\overline{V_0}$, there is a properly supported operator $B_h=\operatorname{Op}_h(b)$, with $b\in C_c^\infty(T^*U)$, such that \begin{align*} B_hA_h=\operatorname{Op}_h(\chi)+C_h+S_h \end{align*} on distributions over $U$, where $S_h$ is residual and $C_h=\operatorname{Op}_h(c)$ has symbol $c\in C_c^\infty(T^*U)$ whose frequency support is disjoint from an open neighbourhood of $V_0$. More concretely, $b$ is chosen equal to $\chi(x)/a(x,\xi)$ on a neighbourhood of $\operatorname{supp}\chi\times\overline{V_0}$, so the full symbol of $\operatorname{Op}_h(\chi)-B_hA_h$ vanishes to all orders in $h$ over $\operatorname{supp}\chi\times V_0$; the remaining nonresidual symbol may therefore be cut off in the complementary frequency region. The hypotheses of this parametrix construction hold here because $a\in C_c^\infty(T^*U)$), $a$ is bounded away from zero on a neighbourhood of $\operatorname{supp}\chi\times\overline{V_0}$, $\operatorname{supp}\chi\Subset U_1$, and $\overline{V_0}\subset V$. Applying this identity to $u_h$ gives \begin{align*} \chi u_h=B_hA_hu_h-C_hu_h-S_hu_h. \end{align*} The term $C_hu_h$ has rapidly small semiclassical Fourier transform on $V_0$. Indeed, let $K_y\Subset U$ be the compact $y$-support supplied by proper support over a fixed compact output set containing $\operatorname{supp}\chi$. Semiclassical temperedness gives integers $m,L\geq0$ and a constant $C_K>0$ controlling the action of $u_h$ on test functions supported in $K_y$. In the Fourier representation of $C_h$ the output frequency $\xi\in V_0$ is separated by a positive distance from the compact frequency support of $c$. Repeated integration by parts in the spatial variables using the nonstationary phase factor $e^{i x\cdot(\eta-\xi)/h}$ therefore gives, after choosing more than $M+L+n+N+m$ integrations by parts, \begin{align*} |\mathcal{F}_h(C_hu_h)(\xi)|\leq C_{N,M}h^M\langle\xi\rangle^{-N} \end{align*} for all $\xi\in V_0$ and all sufficiently small $h$. The constant $C_{N,M}$ depends only on the separation of $V_0$ from the frequency support of $c$, finitely many seminorms of $c$, and the above local distribution seminorm bound for $(u_h)$. Since $A_hu_h=O(h^\infty)$ in $C^\infty_{\mathrm{loc}}(U)$ and $B_h$ is properly supported with compact spatial support over $U_1$, the standard continuity of properly supported semiclassical pseudodifferential operators on local smooth seminorms gives $B_hA_hu_h=O(h^\infty)$ in $C^\infty_{\mathrm{loc}}(U)$. Since $(u_h)$ is semiclassically tempered and $S_h$ is residual, the residual mapping property gives \begin{align*} S_hu_h = O(h^\infty) \end{align*} in $C^\infty(U)$ after multiplication by any compactly supported cutoff. The semiclassical Fourier transform of a compactly supported $O(h^\infty)$ smooth family is $O(h^\infty)\langle\xi\rangle^{-N}$ for every $N$, by repeated integration by parts in the spatial variable. Taking semiclassical Fourier transforms in the preceding decomposition therefore gives, for every $N\geq 0$ and $M\geq 0$, \begin{align*} |\mathcal{F}_h(\chi u_h)(\xi)| \leq C_{N,M}h^M\langle\xi\rangle^{-N} \end{align*} uniformly for $\xi\in V_0$. Replacing $V$ by $V_0$ gives the desired Fourier decay condition.[/step]

[guided]The operator definition says that absence from $\operatorname{WF}_h(u_h)$ is detected by an elliptic pseudodifferential operator that kills $u_h$ to infinite order in $h$. Thus we begin with a compactly supported symbol $a\in C_c^\infty(T^*U)$, elliptic at $(x_0,\xi_0)$, and set $A_h=\operatorname{Op}_h(a)$, with \begin{align*} A_hu_h = O(h^\infty) \end{align*} locally smoothly. Ellipticity is an open condition. Therefore we may choose an open spatial neighbourhood $U_1\Subset U$ of $x_0$ and an open frequency neighbourhood $V\subset\mathbb{R}^n$ of $\xi_0$ such that $a$ remains elliptic on $U_1\times V$. We then choose $\chi:U\to\mathbb{R}$ with $\chi\in C_c^\infty(U_1)$ and $\chi(x_0)\neq 0$. The role of ellipticity is that it permits microlocal division by $a$, but this division must be performed at the level of the full semiclassical symbol, not only at the principal-symbol level. Choose an open neighbourhood $V_0\Subset V$ of $\xi_0$. The semiclassical elliptic parametrix theorem in the properly supported calculus specified in the theorem statement gives a properly supported operator $B_h=\operatorname{Op}_h(b)$ with a compactly supported classical symbol $b\sim\sum_{j=0}^{\infty}h^j b_j$. The leading term satisfies $b_0=\chi(x)/a(x,\xi)$ on a neighbourhood of $\operatorname{supp}\chi\times\overline{V_0}$, and the lower-order terms $b_j$ are chosen recursively by the composition formula so that the full symbol of $\operatorname{Op}_h(\chi)-B_hA_h$ vanishes to every order in $h$ on $\operatorname{supp}\chi\times V_0$. Cutting the remaining full symbol away from $V_0$ gives \begin{align*} B_hA_h=\operatorname{Op}_h(\chi)+C_h+S_h, \end{align*} where $S_h$ is residual and $C_h=\operatorname{Op}_h(c)$ has compactly supported symbol $c$ whose frequency support is disjoint from an open neighbourhood of $V_0$. We verify the hypotheses carefully. The symbol $a$ is compactly supported in $T^*U$. Since $a$ is elliptic on $U_1\times V$, it is bounded away from zero on a neighbourhood of the compact set $\operatorname{supp}\chi\times\overline{V_0}$. This is exactly the region on which division by $a$ is performed. Proper support is part of the quantization convention in the theorem statement, so all operators act on distributions on $U$ by compactly supported kernel slices. Applying the identity to $u_h$ gives \begin{align*} \chi u_h=B_hA_hu_h-C_hu_h-S_hu_h. \end{align*} The first term is rapidly negligible because $A_hu_h=O(h^\infty)$ in local smooth seminorms and properly supported pseudodifferential operators preserve such $O(h^\infty)$ bounds locally. The residual term is rapidly negligible because residual properly supported kernels are $O(h^\infty)$ with all derivatives, and semiclassical temperedness of $(u_h)$ absorbs the fixed polynomial loss in $h^{-1}$ coming from distribution seminorms. It remains to explain why $C_hu_h$ has Fourier decay on $V_0$. The output frequency $\xi\in V_0$ is separated from the frequency support of $c$. In the Fourier representation of $\mathcal{F}_h(C_hu_h)(\xi)$, this separation produces a nonstationary phase factor with derivative proportional to $\eta-\xi$, where $\eta$ is the internal frequency variable of $C_h$. Since $|\eta-\xi|$ is bounded below on the support of the amplitude, repeated integration by parts in the spatial variables gains a factor of $h$ at each integration. Proper support reduces the distributional pairing to a fixed compact set $K_y\Subset U$ in the input variable. Semiclassical temperedness on $K_y$ gives a finite derivative order $m$ and a polynomial loss $h^{-L}$. Choosing the number of integrations by parts larger than this loss, and also larger than the requested powers $M$ and $N$, gives \begin{align*} |\mathcal{F}_h(C_hu_h)(\xi)|\leq C_{N,M}h^M\langle\xi\rangle^{-N} \end{align*} uniformly for $\xi\in V_0$. The constant comes from the separation from the frequency support of $c$, finitely many seminorms of $c$, and the local distribution seminorm bound for $(u_h)$. Combining the estimates for the three terms gives the same bound for $\mathcal{F}_h(\chi u_h)$ on $V_0$. Since $V_0$ is still an open neighbourhood of $\xi_0$, this proves the required Fourier decay direction.[/guided]

[step:Choose an elliptic symbol supported inside the Fourier decay region]Assume conversely that there exist $\chi\in C_c^\infty(U)$ with $\chi(x_0)\neq 0$ and an open neighbourhood $V$ of $\xi_0$ such that the stated Fourier decay estimate holds. Since $\chi(x_0)\neq 0$, choose open sets $W_0\Subset W_1\Subset U$ with $x_0\in W_0$, $\chi$ nowhere zero on $W_1$, and $\overline{W_1}\subset U$. Choose $q:U\to\mathbb{C}$ with $q\in C_c^\infty(W_1)$ and $q\chi=1$ on a neighbourhood of $\overline{W_0}$. Choose an open neighbourhood $V_0\Subset V$ of $\xi_0$. The family $q\chi u_h$ has the same rapid Fourier decay on $V_0$. Indeed, write $q\chi u_h=q(\chi u_h)$. Multiplication by $q\in C_c^\infty(U)$ gives the semiclassical convolution identity \begin{align*} \mathcal{F}_h(q\chi u_h)(\xi)=(2\pi h)^{-n}\int_{\mathbb{R}^n}\mathcal{F}_h q(\xi-\eta)\mathcal{F}_h(\chi u_h)(\eta)\,d\mathcal{L}^n(\eta) \end{align*} for $\xi\in\mathbb{R}^n$, interpreted by the compact support of $q\chi u_h$. By repeated integration by parts in the defining integral for $\mathcal{F}_h q$, for every $R\geq0$ and $J\geq0$ there is $C_{R,J}>0$ such that \begin{align*} |\mathcal{F}_h q(\zeta)|\leq C_{R,J}h^J\langle\zeta\rangle^{-R} \end{align*} for all $\zeta\in\mathbb{R}^n$. Split the $\eta$-integral into $\eta\in V$ and $\eta\notin V$. On $V$, the assumed estimate for $\mathcal{F}_h(\chi u_h)$ gives arbitrary powers of $h$ and $\langle\eta\rangle^{-N}$, and the rapid decay of $\mathcal{F}_h q(\xi-\eta)$ makes the convolution finite uniformly for $\xi\in V_0$. On $\mathbb{R}^n\setminus V$, the positive distance $\operatorname{dist}(V_0,\mathbb{R}^n\setminus V)>0$ allows the same integration-by-parts estimate for $\mathcal{F}_h q(\xi-\eta)$ to supply an arbitrary power of $h$; the remaining polynomial growth of $\mathcal{F}_h(\chi u_h)$ is bounded by the semiclassical temperedness of $(u_h)$ applied to the compactly supported distribution $\chi u_h$. Choosing $R$ and $J$ larger than the requested decay order and the temperedness loss proves the same estimate for $\mathcal{F}_h(q\chi u_h)$ on $V_0$. Choose $\rho:U\to[0,1]$ with $\rho\in C_c^\infty(W_0)$ and $\rho(x_0)\neq 0$. Then $q\chi=1$ on a neighbourhood of $\operatorname{supp}\rho$. Choose $\psi:\mathbb{R}^n\to[0,1]$ with $\psi\in C_c^\infty(V_0)$ and $\psi(\xi_0)\neq 0$. Define \begin{align*} a:T^*U\to\mathbb{C},\qquad a(x,\xi)=\rho(x)\psi(\xi). \end{align*} Then $a\in C_c^\infty(T^*U)$ and $a$ is elliptic at $(x_0,\xi_0)$ because $\rho(x_0)\psi(\xi_0)\neq 0$. Let $A_h=\operatorname{Op}_h(a)$.[/step]

[guided]The point of this step is to build an operator whose symbol is nonzero at $(x_0,\xi_0)$ but whose frequency support lies where the Fourier transform is assumed to be rapidly small. Since $\chi(x_0)\neq 0$, continuity gives a neighbourhood $W_1$ of $x_0$ on which $\chi$ is nowhere zero. We choose $W_0\Subset W_1\Subset U$ with $x_0\in W_0$ and then choose $q\in C_c^\infty(W_1)$ so that $q\chi=1$ on a neighbourhood of $\overline{W_0}$. We must justify that replacing $\chi u_h$ by $q\chi u_h$ does not destroy the Fourier decay. The multiplication is by the fixed compactly supported smooth function $q$, and in frequency space it gives \begin{align*} \mathcal{F}_h(q\chi u_h)(\xi)=(2\pi h)^{-n}\int_{\mathbb{R}^n}\mathcal{F}_h q(\xi-\eta)\mathcal{F}_h(\chi u_h)(\eta)\,d\mathcal{L}^n(\eta). \end{align*} The factor $\mathcal{F}_h q$ is rapidly decaying with arbitrary powers of $h$: repeated integration by parts in the compact $x$-support of $q$ gives \begin{align*} |\mathcal{F}_h q(\zeta)|\leq C_{R,J}h^J\langle\zeta\rangle^{-R} \end{align*} for all $R,J\geq0$. For $\eta\in V$, the assumed rapid estimate controls $\mathcal{F}_h(\chi u_h)(\eta)$. For $\eta\notin V$ and $\xi\in V_0$, the positive distance from $V_0$ to $\mathbb{R}^n\setminus V$ lets us choose $J$ large enough in the estimate for $\mathcal{F}_h q(\xi-\eta)$ to dominate the polynomial $h^{-1}$ loss allowed by semiclassical temperedness of $\chi u_h$. Taking $R$ large makes the convolution integrable with the desired $\langle\xi\rangle^{-N}$ weight. Thus $\mathcal{F}_h(q\chi u_h)$ satisfies the same $O(h^\infty)\langle\xi\rangle^{-N}$ estimate on $V_0$. Now choose $\rho\in C_c^\infty(W_0)$ with $\rho(x_0)\neq 0$ and choose $\psi\in C_c^\infty(V_0)$ with $\psi(\xi_0)\neq 0$. Define the symbol as the map \begin{align*} a:T^*U&\to\mathbb{C} \end{align*} by $a(x,\xi)=\rho(x)\psi(\xi)$. This symbol is compactly supported, and $a(x_0,\xi_0)=\rho(x_0)\psi(\xi_0)\neq 0$, so it is elliptic at $(x_0,\xi_0)$.[/guided]

[step:Show that the operator kills the localized piece]We first prove that $A_h(q\chi u_h)=O(h^\infty)$ in $C^\infty(U)$. Since $q\chi u_h$ has compact support, the Fourier representation of the left quantization gives \begin{align*} A_h(q\chi u_h)(x) = (2\pi h)^{-n}\int_{\mathbb{R}^n} e^{i x\cdot\xi/h} a(x,\xi)\mathcal{F}_h(q\chi u_h)(\xi)\,d\mathcal{L}^n(\xi). \end{align*} Because $\operatorname{supp}\psi\subset V_0$, the integral is taken over a compact subset of $V_0$. For every multi-index $\alpha$, differentiating in $x$ gives a finite sum of terms of the form \begin{align*} (2\pi h)^{-n}h^{-|\beta|}\int_{\operatorname{supp}\psi} e^{i x\cdot\xi/h} c_{\alpha,\beta}(x,\xi)\mathcal{F}_h(q\chi u_h)(\xi)\,d\mathcal{L}^n(\xi), \end{align*} where $c_{\alpha,\beta}\in C_c^\infty(U\times V_0)$ is obtained from derivatives of $a$ and multiplication by monomials in $\xi$. The set $\operatorname{supp}\psi$ is compact, hence has finite $\mathcal{L}^n$-measure, and every monomial in $\xi$ that appears in $c_{\alpha,\beta}$ is bounded on $\operatorname{supp}\psi$. The Fourier decay estimate for $q\chi u_h$, with $M$ replaced by $M+n+|\beta|+1$, therefore bounds each such term by $C_{\alpha,M}h^M$ uniformly for $x$ in compact subsets of $U$; here $C_{\alpha,M}$ is obtained explicitly from the relevant Fourier decay constant, the finite list of seminorms of $a$ appearing in $c_{\alpha,\beta}$, the supremum of the finitely many $\xi$-monomials on $\operatorname{supp}\psi$, and $\mathcal{L}^n(\operatorname{supp}\psi)<\infty$. Therefore \begin{align*} A_h(q\chi u_h)=O(h^\infty) \end{align*} in $C^\infty(U)$.[/step]

[guided]We estimate the operator directly from its Fourier representation. Since $q\chi u_h$ is compactly supported, the formula for left quantization is valid: \begin{align*} A_h(q\chi u_h)(x) = (2\pi h)^{-n}\int_{\mathbb{R}^n} e^{i x\cdot\xi/h} a(x,\xi)\mathcal{F}_h(q\chi u_h)(\xi)\,d\mathcal{L}^n(\xi). \end{align*} Because $a(x,\xi)=\rho(x)\psi(\xi)$ and $\operatorname{supp}\psi\subset V_0$, the integral only sees frequencies where $\mathcal{F}_h(q\chi u_h)$ is rapidly small. If $\alpha$ is a multi-index, differentiating in $x$ differentiates the amplitude and may also differentiate $e^{i x\cdot\xi/h}$; each derivative landing on the exponential contributes a factor $h^{-1}\xi_j$. Therefore every differentiated term is a finite sum of integrals of the form \begin{align*} (2\pi h)^{-n}h^{- |\beta|}\int_{\operatorname{supp}\psi} e^{i x\cdot\xi/h} c_{\alpha,\beta}(x,\xi)\mathcal{F}_h(q\chi u_h)(\xi)\,d\mathcal{L}^n(\xi), \end{align*} where $c_{\alpha,\beta}\in C_c^\infty(U\times V_0)$ is built from derivatives of $a$ and monomials in $\xi$. The constants are finite for concrete reasons: $\operatorname{supp}\psi$ is compact and hence has finite $\mathcal{L}^n$-measure, the finitely many $\xi$-monomials are bounded on $\operatorname{supp}\psi$, and only finitely many seminorms of $a$ occur for a fixed $\alpha$. Taking the Fourier decay estimate for $q\chi u_h$ with the exponent $M+n+|\beta|+1$ absorbs the prefactor $(2\pi h)^{-n}h^{-|\beta|}$. Thus each differentiated term is $O(h^M)$ uniformly on compact subsets of $U$, and consequently \begin{align*} A_h(q\chi u_h)=O(h^\infty) \end{align*} in $C^\infty(U)$.[/guided]

[step:Remove the auxiliary spatial cutoff by nonstationary phase]It remains to control $A_h((1-q\chi)u_h)$. The factor $\rho(x)$ is contained in the symbol $a(x,\xi)=\rho(x)\psi(\xi)$, so the Schwartz kernel only involves $x\in\operatorname{supp}\rho$. Since $q\chi=1$ on a neighbourhood of $\operatorname{supp}\rho$, choose $\theta:U\to[0,1]$ with $\theta\in C_c^\infty(U)$, $\theta=1$ on a neighbourhood of $\operatorname{supp}\rho$, and $q\chi=1$ on a neighbourhood of $\operatorname{supp}\theta$. Then \begin{align*} A_h((1-q\chi)u_h)=A_h((1-q\chi)\theta u_h)+A_h((1-q\chi)(1-\theta)u_h). \end{align*} The first term is identically zero because $(1-q\chi)\theta=0$. For the second term, the spatial supports of $\rho$ and $(1-q\chi)(1-\theta)$ are separated. Thus there exists $\delta>0$ such that \begin{align*} |x-y|\geq \delta \end{align*} whenever $x\in\operatorname{supp}\rho$ and $y\in\operatorname{supp}(1-\theta)$. The Schwartz kernel of $A_h(1-q\chi)(1-\theta)$ is \begin{align*} K_h(x,y)=(2\pi h)^{-n}\int_{\mathbb{R}^n}e^{i(x-y)\cdot\xi/h}a(x,\xi)(1-q(y)\chi(y))(1-\theta(y))\,d\mathcal{L}^n(\xi). \end{align*} Because the quantization in the theorem statement is properly supported, for every compact output set $K_x\Subset U$ there is a compact set $K_y\Subset U$ such that the Schwartz kernel of $A_h$ over $K_x\times U$ is supported in $K_x\times K_y$. Hence, when estimating $A_h((1-q\chi)(1-\theta)u_h)$ on $K_x$, the distribution $u_h$ is applied only to compactly supported test functions in the $y$ variable. For every compact set $K_x\Subset U$, every pair of multi-indices $\alpha$ and $\gamma$, and every $M\geq0$, repeated integration by parts in $\xi$ with \begin{align*} L_{x,y,\xi}=\frac{h}{i|x-y|^2}\sum_{j=1}^n (x_j-y_j)\partial_{\xi_j} \end{align*} on the compact set $(K_x\cap\operatorname{supp}\rho)\times K_y$ gives \begin{align*} \sup_{x\in K_x,\,y\in K_y}|\partial_x^\alpha\partial_y^\gamma K_h(x,y)|\leq C_{\alpha,\gamma,K_x,M}h^M. \end{align*} Here the constants are finite because $|x-y|\geq\delta$ on the support of the amplitude, the $\xi$-support of $a$ is compact, and only finitely many derivatives of $a$, $q\chi$, and $\theta$ occur. Since $(u_h)$ is semiclassically tempered as a distribution on $U$, its action on compactly supported test functions in $K_y$ grows at most polynomially in $h^{-1}$ in local distribution seminorms. Choosing the number of integrations by parts larger than this polynomial loss gives \begin{align*} A_h((1-q\chi)(1-\theta)u_h)=O(h^\infty) \end{align*} in $C^\infty_{\mathrm{loc}}(U)$, and therefore also \begin{align*} A_h((1-q\chi)u_h)=O(h^\infty) \end{align*} in $C^\infty_{\mathrm{loc}}(U)$. Combining this with the previous step gives \begin{align*} A_hu_h=A_h(q\chi u_h)+A_h((1-q\chi)u_h)=O(h^\infty) \end{align*} in $C^\infty_{\mathrm{loc}}(U)$.[/step]

[guided]We still have to remove the auxiliary factor $q\chi$. Since $q\chi=1$ near $\operatorname{supp}\rho$, the symbol of $A_h$ only observes $x$ in a region where $1-q\chi$ vanishes. Choose $\theta\in C_c^\infty(U)$ with $\theta=1$ near $\operatorname{supp}\rho$ and with $q\chi=1$ near $\operatorname{supp}\theta$. Then \begin{align*} A_h((1-q\chi)u_h)=A_h((1-q\chi)\theta u_h)+A_h((1-q\chi)(1-\theta)u_h). \end{align*} The first term is zero because $(1-q\chi)\theta=0$. For the second term, the $x$-support of the operator is contained in $\operatorname{supp}\rho$, while the $y$-support of $(1-\theta)$ is separated from $\operatorname{supp}\rho$. Thus there is $\delta>0$ such that $|x-y|\geq\delta$ on the relevant support. The proper support assumption in the theorem statement is essential here: on each compact output set $K_x\Subset U$, the kernel only pairs $u_h$ with test functions supported in some compact set $K_y\Subset U$. Therefore the distribution $u_h$ is being applied legitimately. On $K_x\times K_y$, repeated integration by parts in $\xi$ with \begin{align*} L_{x,y,\xi}=\frac{h}{i|x-y|^2}\sum_{j=1}^n (x_j-y_j)\partial_{\xi_j} \end{align*} gains one factor of $h$ each time because the phase derivative is bounded below by $\delta$. The compact $\xi$-support of $a$ and the finite number of derivatives of $a$, $q\chi$, and $\theta$ control the constants. After enough integrations by parts, the resulting $h^M$ gain dominates the polynomial $h^{-1}$ growth allowed by semiclassical temperedness of $(u_h)$. Hence \begin{align*} A_h((1-q\chi)u_h)=O(h^\infty) \end{align*} in $C^\infty_{\mathrm{loc}}(U)$. Combining this estimate with $A_h(q\chi u_h)=O(h^\infty)$ gives $A_hu_h=O(h^\infty)$ locally smoothly.[/guided]

[step:Conclude the equivalence with the operator definition] The symbol $a(x,\xi)=\rho(x)\psi(\xi)$ is compactly supported and elliptic at $(x_0,\xi_0)$, and the corresponding semiclassical operator satisfies \begin{align*} A_hu_h=O(h^\infty) \end{align*} locally smoothly. By the operator-theoretic definition of the semiclassical wavefront set, this means \begin{align*} (x_0,\xi_0)\notin\operatorname{WF}_h(u_h). \end{align*} Together with the first direction, this proves the equivalence. [/step]