[proofplan]
The proof is a bookkeeping application of the semiclassical sharp Gårding inequality. First we verify that the localized zero extension $q=\chi^2 b$ is a real globally nonnegative order-zero symbol on $\mathbb{R}^n$, with seminorms controlled by the stated local seminorms of $b$ and $\chi$. Sharp Gårding then gives the Euclidean lower bound for $\operatorname{Op}_h(q)$ on $T_\rho u$. Finally, the smooth positive density in the coordinate chart compares the Euclidean norm of $T_\rho u$ with the intrinsic $L^2(M,d\mu)$ norm.
[/proofplan]
[step:Verify that the zero extension is a real nonnegative order-zero symbol]
Choose an open set $W_0$ such that $\operatorname{supp}\chi\subset W_0$, $\overline{W_0}\subset W$, and $b(x,\xi;h)\ge 0$ for all $(x,\xi,h)\in W_0\times\mathbb{R}^n\times(0,h_0]$. Since $\chi\in C_c^\infty(V;\mathbb{R})$, the function $\chi^2 b$ vanishes for $x$ outside the compact set $\operatorname{supp}\chi\subset V$. Hence its zero extension $q$ is smooth in the $x$ variable across $\partial V$.
The symbol $q$ is real-valued because both $\chi$ and $b$ are real-valued. It is also globally nonnegative: if $x\in\operatorname{supp}\chi$, then $x\in W_0$ and
\begin{align*}
q(x,\xi;h)=\chi(x)^2b(x,\xi;h)\ge 0.
\end{align*}
If $x\notin\operatorname{supp}\chi$, then $\chi(x)=0$ on $V$ and the zero extension also gives $q(x,\xi;h)=0$ outside $V$.
For multi-indices $\alpha,\beta\in\mathbb{N}_0^n$, the Leibniz rule gives each derivative $\partial_x^\alpha\partial_\xi^\beta q$ on $V$ as a finite sum of products of derivatives of $\chi^2$ of order at most $|\alpha|$ and derivatives of $b$ of order at most $|\alpha|+|\beta|$. Because the $x$-support of $q$ is contained in the fixed compact set $\operatorname{supp}\chi$, the corresponding $S^0$ seminorms of $q$ are bounded by finitely many $C^k$ seminorms of $\chi$ and finitely many $S^0$ seminorms of $b$ on a fixed neighbourhood of $\operatorname{supp}\chi\times\mathbb{R}^n$.
[guided]
The point of the cutoff is to turn a local nonnegativity assumption into a global symbol to which sharp Gårding can be applied. We choose an open set $W_0$ satisfying
\begin{align*}
\operatorname{supp}\chi\subset W_0\subset \overline{W_0}\subset W.
\end{align*}
This is possible because $\operatorname{supp}\chi$ is compactly contained in $V$ and the hypothesis gives nonnegativity on a neighbourhood $W$ of $\operatorname{supp}\chi$.
Now define $q$ as the zero extension of $\chi^2 b$. There are two points to check. First, the zero extension is smooth. Since $\chi\in C_c^\infty(V;\mathbb{R})$, the function $\chi$ vanishes in a neighbourhood of $\partial V$. Therefore $\chi^2 b$ also vanishes in a neighbourhood of $\partial V$, so extending it by zero outside $V$ introduces no jump and no loss of smoothness.
Second, $q$ is nonnegative on all of $\mathbb{R}^n\times\mathbb{R}^n$. If $x\in\operatorname{supp}\chi$, then $x\in W_0$, and the hypothesis gives $b(x,\xi;h)\ge 0$. Since $\chi(x)^2\ge 0$, we get
\begin{align*}
q(x,\xi;h)=\chi(x)^2b(x,\xi;h)\ge 0.
\end{align*}
If $x\notin\operatorname{supp}\chi$, then $\chi(x)=0$ when $x\in V$, while the zero extension gives $q(x,\xi;h)=0$ when $x\notin V$. Thus $q\ge 0$ everywhere.
Finally, $q$ remains an order-zero semiclassical symbol. For every pair of multi-indices $\alpha,\beta\in\mathbb{N}_0^n$, the Leibniz rule expresses $\partial_x^\alpha\partial_\xi^\beta(\chi^2b)$ as a finite sum of terms of the form
\begin{align*}
(\partial_x^\gamma\chi^2)(x)(\partial_x^{\alpha-\gamma}\partial_\xi^\beta b)(x,\xi;h)
\end{align*}
with $\gamma\le\alpha$. The derivatives of $\chi^2$ are bounded because $\chi$ is smooth and compactly supported, and the derivatives of $b$ are controlled by the assumed $S^0$ seminorm bounds on the fixed neighbourhood where $\chi$ is supported. This proves the stated seminorm dependence for $q$.
[/guided]
[/step]
[step:Apply semiclassical sharp Gårding to the localized symbol]
By the semiclassical sharp Gårding inequality for left Kohn--Nirenberg quantization, applied to the real nonnegative symbol $q\in S^0(\mathbb{R}^n\times\mathbb{R}^n)$, there exist constants $C_G>0$ and $h_G\in(0,h_0]$ such that for every $v\in C_c^\infty(\mathbb{R}^n)$ and every $0<h\le h_G$,
\begin{align*}
\operatorname{Re}\bigl(\operatorname{Op}_h(q)v,v\bigr)_{L^2(\mathbb{R}^n)}\ge -C_G h\|v\|_{L^2(\mathbb{R}^n)}^2.
\end{align*}
The hypotheses of this inequality are satisfied by the previous step: $q$ is real, globally nonnegative, and belongs to $S^0$ with the required finite seminorm bounds. Taking $v=T_\rho u$ gives
\begin{align*}
\operatorname{Re}\bigl(\operatorname{Op}_h(q)T_\rho u,T_\rho u\bigr)_{L^2(\mathbb{R}^n)}\ge -C_G h\|T_\rho u\|_{L^2(\mathbb{R}^n)}^2.
\end{align*}
[guided]
The analytic input is the semiclassical sharp Gårding inequality for left Kohn--Nirenberg quantization. It applies to a real-valued globally nonnegative symbol in $S^0(\mathbb{R}^n\times\mathbb{R}^n)$ whose relevant symbol seminorms are uniformly bounded for $0<h\le h_0$. The previous step verified exactly these hypotheses for $q$: it is real-valued, satisfies $q(x,\xi;h)\ge 0$ for all $(x,\xi)\in\mathbb{R}^n\times\mathbb{R}^n$, and has order-zero seminorms controlled by finitely many local seminorms of $b$ and finitely many seminorms of $\chi$.
Therefore there exist constants $C_G>0$ and $h_G\in(0,h_0]$, depending only on those finite seminorm bounds, such that for every $v\in C_c^\infty(\mathbb{R}^n)$ and every $0<h\le h_G$,
\begin{align*}
\operatorname{Re}\bigl(\operatorname{Op}_h(q)v,v\bigr)_{L^2(\mathbb{R}^n)}\ge -C_G h\|v\|_{L^2(\mathbb{R}^n)}^2.
\end{align*}
The localization map $T_\rho$ sends each $u\in C^\infty(M)$ to a compactly supported smooth function on $\mathbb{R}^n$, because $\rho\in C_c^\infty(V)$ and the definition extends by zero outside $V$. Hence $v=T_\rho u$ is an admissible test function in the sharp Gårding estimate, and substituting it gives
\begin{align*}
\operatorname{Re}\bigl(\operatorname{Op}_h(q)T_\rho u,T_\rho u\bigr)_{L^2(\mathbb{R}^n)}\ge -C_G h\|T_\rho u\|_{L^2(\mathbb{R}^n)}^2.
\end{align*}
[/guided]
[/step]
[step:Compare the Euclidean localized norm with the manifold norm]
Let $m:V\to(0,\infty)$ be the smooth density coefficient defined by the pullback identity
\begin{align*}
(\kappa^{-1})^*d\mu=m(x)\,d\mathcal{L}^n(x).
\end{align*}
Because $\operatorname{supp}\rho$ is compact in $V$ and $m$ is positive and smooth, the constant
\begin{align*}
A_\rho=\sup_{x\in\operatorname{supp}\rho}\frac{|\rho(x)|^2}{m(x)}
\end{align*}
is finite. For $u\in C^\infty(M)$, the definition of $T_\rho$ gives
\begin{align*}
\|T_\rho u\|_{L^2(\mathbb{R}^n)}^2=\int_V |\rho(x)|^2 |u(\kappa^{-1}(x))|^2\,d\mathcal{L}^n(x).
\end{align*}
By the definition of $A_\rho$,
\begin{align*}
\|T_\rho u\|_{L^2(\mathbb{R}^n)}^2\le A_\rho\int_V |u(\kappa^{-1}(x))|^2m(x)\,d\mathcal{L}^n(x).
\end{align*}
Using the density pullback formula, the integral on the right equals the $L^2$ mass of $u$ over $U$:
\begin{align*}
\int_V |u(\kappa^{-1}(x))|^2m(x)\,d\mathcal{L}^n(x)=\int_U |u(p)|^2\,d\mu(p).
\end{align*}
Since $U\subset M$, we conclude
\begin{align*}
\|T_\rho u\|_{L^2(\mathbb{R}^n)}^2\le A_\rho\|u\|_{L^2(M,d\mu)}^2.
\end{align*}
[guided]
We now translate the Euclidean norm produced by sharp Gårding back to the intrinsic $L^2$ norm on $M$. The density $d\mu$ is smooth and positive, so in the chart $\kappa:U\to V$ there is a smooth function $m:V\to(0,\infty)$ such that
\begin{align*}
(\kappa^{-1})^*d\mu=m(x)\,d\mathcal{L}^n(x).
\end{align*}
This identity means that integration over $U$ with respect to $d\mu$ becomes integration over $V$ with respect to the weighted Lebesgue measure $m(x)\,d\mathcal{L}^n(x)$.
Because $\rho$ is compactly supported in $V$ and $m$ is positive and continuous, the ratio $|\rho(x)|^2/m(x)$ is bounded on $\operatorname{supp}\rho$. Define
\begin{align*}
A_\rho=\sup_{x\in\operatorname{supp}\rho}\frac{|\rho(x)|^2}{m(x)}.
\end{align*}
Then $A_\rho<\infty$, and the definition of $T_\rho$ gives
\begin{align*}
\|T_\rho u\|_{L^2(\mathbb{R}^n)}^2=\int_V |\rho(x)|^2 |u(\kappa^{-1}(x))|^2\,d\mathcal{L}^n(x).
\end{align*}
Using $|\rho(x)|^2\le A_\rho m(x)$ on $\operatorname{supp}\rho$, we obtain
\begin{align*}
\|T_\rho u\|_{L^2(\mathbb{R}^n)}^2\le A_\rho\int_V |u(\kappa^{-1}(x))|^2m(x)\,d\mathcal{L}^n(x).
\end{align*}
The chart-density formula identifies the last integral with
\begin{align*}
\int_U |u(p)|^2\,d\mu(p).
\end{align*}
Since $U\subset M$, this is bounded above by $\|u\|_{L^2(M,d\mu)}^2$. Therefore
\begin{align*}
\|T_\rho u\|_{L^2(\mathbb{R}^n)}^2\le A_\rho\|u\|_{L^2(M,d\mu)}^2.
\end{align*}
[/guided]
[/step]
[step:Combine the Gårding estimate with the chart-density comparison]
Set $h_1=h_G$ and $C=C_GA_\rho$. Combining the sharp Gårding bound with the norm comparison gives, for every $u\in C^\infty(M)$ and every $0<h\le h_1$,
\begin{align*}
\operatorname{Re}\bigl(\operatorname{Op}_h(q)T_\rho u,T_\rho u\bigr)_{L^2(\mathbb{R}^n)}\ge -C_G h\|T_\rho u\|_{L^2(\mathbb{R}^n)}^2.
\end{align*}
Using $\|T_\rho u\|_{L^2(\mathbb{R}^n)}^2\le A_\rho\|u\|_{L^2(M,d\mu)}^2$, this becomes
\begin{align*}
\operatorname{Re}\bigl(\operatorname{Op}_h(q)T_\rho u,T_\rho u\bigr)_{L^2(\mathbb{R}^n)}\ge -Ch\|u\|_{L^2(M,d\mu)}^2.
\end{align*}
The dependence of $C$ and $h_1$ is precisely the dependence inherited from the finite symbol seminorms in sharp Gårding and from the fixed chart-density comparison constant $A_\rho$. This proves the localized semiclassical sharp Gårding estimate.
[guided]
The sharp Gårding step gives the Euclidean lower bound
\begin{align*}
\operatorname{Re}\bigl(\operatorname{Op}_h(q)T_\rho u,T_\rho u\bigr)_{L^2(\mathbb{R}^n)}\ge -C_G h\|T_\rho u\|_{L^2(\mathbb{R}^n)}^2
\end{align*}
for every $0<h\le h_G$. The norm comparison step gives
\begin{align*}
\|T_\rho u\|_{L^2(\mathbb{R}^n)}^2\le A_\rho\|u\|_{L^2(M,d\mu)}^2.
\end{align*}
Combining these two inequalities yields
\begin{align*}
\operatorname{Re}\bigl(\operatorname{Op}_h(q)T_\rho u,T_\rho u\bigr)_{L^2(\mathbb{R}^n)}\ge -C_GA_\rho h\|u\|_{L^2(M,d\mu)}^2.
\end{align*}
Set $h_1=h_G$ and $C=C_GA_\rho$. The constant $C_G$ and threshold $h_G$ come from sharp Gårding and depend only on finitely many order-zero seminorms of $q$; the first step bounded those seminorms by finitely many local seminorms of $b$ and finitely many $C^k$ seminorms of $\chi$. The factor $A_\rho$ is exactly the chart-density norm comparison constant determined by $\rho$ and the positive density coefficient $m$. Thus the asserted estimate holds for every $u\in C^\infty(M)$ and every $0<h\le h_1$.
[/guided]
[/step]
