[proofplan]
The proof treats the sharp Gårding inequality as the order-zero Weyl-quantization corollary of the semiclassical Fefferman-Phong lower bound. That external result says that a real nonnegative symbol has Weyl quantization bounded below by a constant times $-h$ on $L^2$, with the constant controlled by finitely many symbol seminorms. We state that lower bound precisely, verify that the present symbol $a$ satisfies all of its hypotheses, and then set $C := C_{\mathrm{FP}}$ and $h_0 := h_{\mathrm{FP}}$ to obtain the claimed estimate for each Schwartz function $u$.
[/proofplan]
[step:Record the semiclassical Fefferman-Phong lower bound needed here]
We use the following standard semiclassical Fefferman-Phong estimate as the external prerequisite for this corollary: if $b \in S^0(T^*\mathbb{R}^n)$ is real-valued and satisfies $b(x,\xi) \geq 0$ for all $(x,\xi) \in T^*\mathbb{R}^n$, then there exist an integer $N \in \mathbb{N}$ and constants $C_{\mathrm{FP}} > 0$ and $h_{\mathrm{FP}} > 0$, depending only on $n$ and on the seminorms
\begin{align*}
\sup_{(x,\xi) \in \mathbb{R}^n \times \mathbb{R}^n} \langle \xi \rangle^{|\beta|} |\partial_x^\alpha \partial_\xi^\beta b(x,\xi)|, \qquad |\alpha| + |\beta| \leq N,
\end{align*}
such that
\begin{align*}
(\operatorname{Op}_h^w(b)v,v)_{L^2(\mathbb{R}^n)} \geq -C_{\mathrm{FP}} h \|v\|_{L^2(\mathbb{R}^n)}^2
\end{align*}
for every $v \in \mathcal{S}(\mathbb{R}^n)$ and every $h \in (0,h_{\mathrm{FP}}]$.
Here $\operatorname{Op}_h^w(b)$ denotes semiclassical Weyl quantization, namely the operator initially defined on $\mathcal{S}(\mathbb{R}^n)$ by
\begin{align*}
\operatorname{Op}_h^w(b)v(x) = (2\pi h)^{-n}\int_{\mathbb{R}^n}\int_{\mathbb{R}^n} e^{i(x-y)\cdot \xi/h} b\left(\frac{x+y}{2},\xi\right)v(y)\, d\mathcal{L}^n(y)\, d\mathcal{L}^n(\xi),
\end{align*}
understood in the usual oscillatory-integral sense.
[guided]
The only deep input in this proof is the lower-bound theorem just stated. Its content is not merely boundedness of $\operatorname{Op}_h^w(b)$ on $L^2(\mathbb{R}^n)$; it uses the nonnegativity of the symbol $b$ to produce a one-sided estimate for the Weyl quantization. The estimate is weaker than the pointwise inequality $b \geq 0$ might suggest because Weyl quantization does not preserve positivity exactly.
We state the external theorem in the exact normalization needed here. It applies to a real-valued symbol, that is, to a map
\begin{align*}
b: T^*\mathbb{R}^n \cong \mathbb{R}^n \times \mathbb{R}^n \to \mathbb{R},
\end{align*}
with $b \in S^0(T^*\mathbb{R}^n)$ and $b(x,\xi) \geq 0$ for every $(x,\xi) \in T^*\mathbb{R}^n$. The relevant finite family of symbol seminorms has the form
\begin{align*}
\sup_{(x,\xi) \in \mathbb{R}^n \times \mathbb{R}^n} \langle \xi \rangle^{|\beta|} |\partial_x^\alpha \partial_\xi^\beta b(x,\xi)|, \qquad |\alpha| + |\beta| \leq N,
\end{align*}
where $N \in \mathbb{N}$ is supplied by the Fefferman-Phong estimate.
For every $v \in \mathcal{S}(\mathbb{R}^n)$, the Weyl quantization is the oscillatory integral
\begin{align*}
\operatorname{Op}_h^w(b)v(x) = (2\pi h)^{-n}\int_{\mathbb{R}^n}\int_{\mathbb{R}^n} e^{i(x-y)\cdot \xi/h} b\left(\frac{x+y}{2},\xi\right)v(y)\, d\mathcal{L}^n(y)\, d\mathcal{L}^n(\xi).
\end{align*}
Both integrations specify Lebesgue measure: $d\mathcal{L}^n(y)$ in the spatial variable and $d\mathcal{L}^n(\xi)$ in the frequency variable. The conclusion of the external theorem is the quadratic-form estimate
\begin{align*}
(\operatorname{Op}_h^w(b)v,v)_{L^2(\mathbb{R}^n)} \geq -C_{\mathrm{FP}} h \|v\|_{L^2(\mathbb{R}^n)}^2
\end{align*}
for all $v \in \mathcal{S}(\mathbb{R}^n)$ and all $h \in (0,h_{\mathrm{FP}}]$.
We now verify the hypotheses for the symbol in the theorem. The given symbol is a map
\begin{align*}
a: T^*\mathbb{R}^n \to \mathbb{R},
\end{align*}
with $a \in S^0(T^*\mathbb{R}^n)$ by hypothesis. It is real-valued by hypothesis, and it satisfies
\begin{align*}
a(x,\xi) \geq 0
\end{align*}
for every $(x,\xi) \in T^*\mathbb{R}^n$ by hypothesis. Thus every assumption of the semiclassical Fefferman-Phong estimate is satisfied with $b := a$.
Applying the estimate with $b := a$ and $v := u$ gives
\begin{align*}
(\operatorname{Op}_h^w(a)u,u)_{L^2(\mathbb{R}^n)} \geq -C_{\mathrm{FP}} h \|u\|_{L^2(\mathbb{R}^n)}^2
\end{align*}
for every $u \in \mathcal{S}(\mathbb{R}^n)$ and every $h \in (0,h_{\mathrm{FP}}]$. Define the constants in the statement by
\begin{align*}
C := C_{\mathrm{FP}}, \qquad h_0 := h_{\mathrm{FP}}.
\end{align*}
Then
\begin{align*}
(\operatorname{Op}_h^w(a)u,u)_{L^2(\mathbb{R}^n)} \geq -Ch \|u\|_{L^2(\mathbb{R}^n)}^2
\end{align*}
for every $u \in \mathcal{S}(\mathbb{R}^n)$ and every $h \in (0,h_0]$. The constants have exactly the finite-seminorm dependence asserted in the theorem, because they are the constants supplied by the Fefferman-Phong estimate for $b := a$.
[/guided]
[/step]
[step:Verify that the given symbol satisfies the hypotheses of the lower bound]
The symbol in the theorem is a map
\begin{align*}
a: T^*\mathbb{R}^n \to \mathbb{R}
\end{align*}
with $a \in S^0(T^*\mathbb{R}^n)$ by hypothesis. It is real-valued and satisfies $a(x,\xi) \geq 0$ for every $(x,\xi) \in T^*\mathbb{R}^n$, again by hypothesis. Therefore $a$ satisfies every assumption of the semiclassical Fefferman-Phong estimate with $b := a$.
[/step]
[step:Apply the lower bound to obtain the sharp Gårding estimate]
Applying the semiclassical Fefferman-Phong estimate with $b := a$ and $v := u$ gives constants $C_{\mathrm{FP}} > 0$ and $h_{\mathrm{FP}} > 0$ such that
\begin{align*}
(\operatorname{Op}_h^w(a)u,u)_{L^2(\mathbb{R}^n)} \geq -C_{\mathrm{FP}} h \|u\|_{L^2(\mathbb{R}^n)}^2
\end{align*}
for every $u \in \mathcal{S}(\mathbb{R}^n)$ and every $h \in (0,h_{\mathrm{FP}}]$.
Define
\begin{align*}
C := C_{\mathrm{FP}}, \qquad h_0 := h_{\mathrm{FP}}.
\end{align*}
The same estimate becomes
\begin{align*}
(\operatorname{Op}_h^w(a)u,u)_{L^2(\mathbb{R}^n)} \geq -Ch \|u\|_{L^2(\mathbb{R}^n)}^2
\end{align*}
for every $u \in \mathcal{S}(\mathbb{R}^n)$ and every $h \in (0,h_0]$.
The dependence of $C$ and $h_0$ is exactly the finite-seminorm dependence inherited from the Fefferman-Phong estimate, namely dependence only on $n$ and on finitely many seminorms of $a$ in $S^0(T^*\mathbb{R}^n)$. This proves the claimed sharp Gårding inequality.
[/step]
