[proofplan]
We reduce the statement to Lewy's classical local non-solvability theorem for the first-order complex vector field whose real and imaginary parts bracket-generate the missing real direction at the origin. The only normalization issue is the factor $1/2$ in $\partial_{\bar z}$; multiplying a differential equation by a non-zero complex scalar does not affect local solvability. The classical theorem supplies a single smooth right-hand side whose equation has no distributional solution on any sufficiently small neighbourhood of the origin, which gives exactly the stated quantifiers.
[/proofplan]
[step:State the classical Lewy obstruction in the required normalization]
We use the following classical theorem of Lewy, stated here as an external prerequisite not yet in the wiki: there exist an open neighbourhood $U_0\subset\mathbb R^3$ of $0$ and a function $g\in C^\infty(U_0;\mathbb C)$ such that, for every open neighbourhood $V\subset U_0$ of $0$, there is no distribution $v\in\mathcal D'(V)$ satisfying
\begin{align*}
\left(\partial_x+i\partial_y+2iz\,\partial_t\right)v=g|_V
\end{align*}
in $\mathcal D'(V)$.
Here $z=x+iy$, and the differential operator
\begin{align*}P:C^\infty(U_0;\mathbb C)\to C^\infty(U_0;\mathbb C), \qquad \phi \mapsto \partial_x\phi+i\partial_y\phi+2iz\,\partial_t\phi.\end{align*}
is extended to distributions by duality with its formal adjoint on compactly supported test functions.
[guided]
The theorem we need from Lewy is not a general existence theorem; it is an obstruction theorem for one explicit complex vector field. It says that the operator
\begin{align*}P:C^\infty(U_0;\mathbb C)\to C^\infty(U_0;\mathbb C), \qquad \phi \mapsto \partial_x\phi+i\partial_y\phi+2iz\,\partial_t\phi.\end{align*}
has a smooth right-hand side $g\in C^\infty(U_0;\mathbb C)$ for which the equation $Pv=g$ has no distributional solution near the origin.
The quantifier is important. Lewy's theorem gives one function $g$, not a different function for each neighbourhood. For this one $g$, every open neighbourhood $V\subset U_0$ of $0$ fails to admit a distribution $v\in\mathcal D'(V)$ with
\begin{align*}
Pv=g|_V
\end{align*}
in $\mathcal D'(V)$.
The mechanism behind the theorem is the standard Lewy adjoint-test-function argument: hypothetical local solvability would imply a fixed a priori estimate for the formal adjoint on smaller neighbourhoods, while Lewy's oscillatory test functions make the adjoint side rapidly small and keep the pairing with a chosen smooth right-hand side non-negligible. That contradiction is the classical non-solvability result being invoked here.
[/guided]
[/step]
[step:Convert Lewy's operator to the Wirtinger form in the statement]
By the definition
\begin{align*}\partial_{\bar z}=\frac{1}{2}(\partial_x+i\partial_y),\end{align*}
the operator in the theorem statement is
\begin{align*}L:C^\infty(U_0;\mathbb C)\to C^\infty(U_0;\mathbb C), \qquad \phi \mapsto \partial_{\bar z}\phi+iz\,\partial_t\phi.\end{align*}
Therefore, for every $\phi\in C^\infty(U_0;\mathbb C)$,
\begin{align*}
2L\phi=(\partial_x+i\partial_y+2iz\,\partial_t)\phi=P\phi.
\end{align*}
The same identity holds in $\mathcal D'(V)$ for every [open set](/page/Open%20Set) $V\subset U_0$, because distributional derivatives and multiplication by the smooth function $z$ are compatible with multiplication of the operator by the scalar $2$.
[/step]
[step:Choose the right-hand side and prove non-solvability on every smaller neighbourhood]
Set
\begin{align*}
U:=U_0
\end{align*}
and define
\begin{align*}f:U\to\mathbb C, \qquad (z,t)\mapsto \frac{1}{2}g(z,t).\end{align*}
Then $f\in C^\infty(U;\mathbb C)$.
Let $V\subset U$ be any open neighbourhood of $0$. Suppose, toward a contradiction, that there exists $u\in\mathcal D'(V)$ such that
\begin{align*}
Lu=f|_V
\end{align*}
in $\mathcal D'(V)$. Multiplying both sides by $2$ in the complex [vector space](/page/Vector%20Space) $\mathcal D'(V)$ gives
\begin{align*}
2Lu=2f|_V.
\end{align*}
Using $2L=P$ and $2f=g$, this becomes
\begin{align*}
Pu=g|_V
\end{align*}
in $\mathcal D'(V)$, contradicting the classical Lewy obstruction stated above. Hence no such distribution $u$ exists on $V$.
Since $V\subset U$ was an arbitrary open neighbourhood of $0$, the same function $f$ is not locally solvable on any neighbourhood of the origin. This proves the theorem.
[/step]
