## Formalized Name
Basic Fefferman-Phong Inequality
## Formalized Statement
Let $n \in \mathbb{N}$. For each pair of multi-indices $\alpha,\beta \in \mathbb{N}_0^n$, define the order-two Euclidean symbol seminorm $q_{\alpha\beta}$ on smooth functions $a: \mathbb{R}^n \times \mathbb{R}^n \to \mathbb{R}$ by
\begin{align*}
q_{\alpha\beta}(a) := \sup_{(x,\xi) \in \mathbb{R}^n \times \mathbb{R}^n} \langle \xi\rangle^{-2+|\beta|}|\partial_x^\alpha \partial_\xi^\beta a(x,\xi)|.
\end{align*}
Here $\langle \xi\rangle := (1 + |\xi|^2)^{1/2}$ for $\xi \in \mathbb{R}^n$. Let
\begin{align*}
a: T^*\mathbb{R}^n \cong \mathbb{R}^n \times \mathbb{R}^n \to \mathbb{R}
\end{align*}
be a real-valued smooth symbol in the standard semiclassical Euclidean symbol class $S(\langle \xi\rangle^2)$, meaning that $q_{\alpha\beta}(a) < \infty$ for every pair of multi-indices $\alpha,\beta \in \mathbb{N}_0^n$. Assume that
\begin{align*}
a(x,\xi) \geq 0
\end{align*}
for every $(x,\xi) \in T^*\mathbb{R}^n$. For $0<h\leq 1$, let
\begin{align*}
\operatorname{Op}_h^w(a):\mathcal{S}(\mathbb{R}^n)\to \mathcal{S}'(\mathbb{R}^n)
\end{align*}
denote the semiclassical Weyl quantization, defined for $u\in\mathcal{S}(\mathbb{R}^n)$ and $x\in\mathbb{R}^n$ by the oscillatory integral
\begin{align*}
\operatorname{Op}_h^w(a)u(x) = (2\pi h)^{-n} \int_{\mathbb{R}^n} \int_{\mathbb{R}^n} e^{\frac{i}{h}(x-y)\cdot \xi} a\left(\frac{x+y}{2},\xi\right) u(y)\, d\mathcal{L}^n(\xi)\, d\mathcal{L}^n(y).
\end{align*}
Let the $L^2(\mathbb{R}^n)$ inner product be defined by
\begin{align*}
(v,w)_{L^2(\mathbb{R}^n)} := \int_{\mathbb{R}^n} v(x)\overline{w(x)}\, d\mathcal{L}^n(x)
\end{align*}
for $v,w \in L^2(\mathbb{R}^n)$. Then there exist an integer $N \in \mathbb{N}$, a constant $C>0$, and a constant $h_0 \in (0,1]$, with $C$ and $h_0$ depending only on $n$ and on the finite family of seminorms $\{q_{\alpha\beta}(a): |\alpha|+|\beta|\leq N\}$, such that
\begin{align*}
(\operatorname{Op}_h^w(a)u,u)_{L^2(\mathbb{R}^n)} \geq -C h^2 \|u\|_{L^2(\mathbb{R}^n)}^2
\end{align*}
for every $u\in \mathcal{S}(\mathbb{R}^n)$ and every $0<h\leq h_0$.
## Proof
[proofplan]
The approved material does not match this theorem. The only safe edit is to preserve the existing deferred status while adding the required proof structure tags, since no Fefferman-Phong localization argument is available in the current proof text.
[/proofplan]
[step:Record that the available plan does not prove the Fefferman-Phong inequality]
PROOF_DEFERRED: the approved proof plan is for coordinate invariance of principal symbols of pseudodifferential operators on half-densities, not for the Fefferman-Phong inequality. A complete proof of this theorem requires a genuine Fefferman-Phong localization argument or an existing Fefferman-Phong theorem in the database to cite; neither is supplied by the approved plan.
[guided]
The approved plan addresses coordinate invariance of principal symbols on half-densities, which is not the same statement as the Basic Fefferman-Phong Inequality. Since no Fefferman-Phong localization argument or existing theorem citation is present in the current proof text, the proof remains deferred rather than being rewritten to a different argument.
PROOF_DEFERRED: the approved proof plan is for coordinate invariance of principal symbols of pseudodifferential operators on half-densities, not for the Fefferman-Phong inequality. A complete proof of this theorem requires a genuine Fefferman-Phong localization argument or an existing Fefferman-Phong theorem in the database to cite; neither is supplied by the approved plan.
[/guided]
[/step]
