[proofplan] We fix the sign convention by using the defining function $\rho$ that is positive on the prescribed side $\Omega^+$. The statement has been made explicitly conditional on Lewy's local one-sided [extension theorem](/theorems/59), whose sign convention says that a positive Levi eigenvalue for $\rho$ gives extension into the negative side $\{\rho<0\}$. The proof verifies that the present hypersurface, defining function, Levi-form hypothesis, and CR datum satisfy that analytic input, and then records the resulting boundary trace identity. [/proofplan] [step:Normalize the hypersurface and the positive side] Let $\rho:U\to\mathbb R$ be the chosen $C^\infty$ defining function, with $\Omega^+\cap U=\{\rho>0\}$. Since $d\rho_p\ne 0$, after shrinking $U$ and applying a holomorphic affine change of coordinates sending $p$ to $0$, we may assume that the complex tangent space is \begin{align*} T^{1,0}_0M=\operatorname{span}_{\mathbb C}\left\{\frac{\partial}{\partial z_1},\dots,\frac{\partial}{\partial z_{n-1}}\right\}. \end{align*} Write the normal complex coordinate as $z_n=s+it$, where $s:=\operatorname{Re} z_n$ and $t:=\operatorname{Im} z_n$ are real coordinate functions on the last complex factor. The hypothesis says that the Hermitian form $\mathcal L_{\rho,0}$ has a vector $L\in T^{1,0}_0M$ with \begin{align*} \mathcal L_{\rho,0}(L,L)>0. \end{align*} After a unitary change in the tangential variables, we may take $L=\partial/\partial z_1$ at $0$. With the convention $\Omega^+=\{\rho>0\}$, the local Lewy sign convention is that a positive eigenvalue of $\mathcal L_{\rho,0}$ produces extension into the side on which the defining function is negative, namely $\Omega^-\cap U=\{\rho<0\}$. [/step] [step:Apply the stated Lewy analytic input on the opposite side] Let $u\in C^\infty(M\cap U;\mathbb C)$ satisfy $\bar\partial_bu=0$ on $M\cap U$. Define the antiholomorphic CR tangent bundle by $T^{0,1}M:=\overline{T^{1,0}M}$; the condition $\bar\partial_bu=0$ means that every smooth local section of $T^{0,1}M$ annihilates $u$ on $M\cap U$. We apply the analytic input stated in the theorem with defining function $r:=\rho$ and base point $p$. Its hypotheses are: $M$ is a $C^\infty$ real hypersurface, $r$ is a $C^\infty$ local defining function with $dr\ne 0$ on $M\cap U$, $u$ is a smooth CR function on $M\cap U$, and $\mathcal L_{r,p}$ has a positive eigenvalue. Since $r=\rho$, these hypotheses are exactly the assumptions in the theorem statement. The conclusion of the analytic input applies to the side $\{r<0\}=\{\rho<0\}=\Omega^-\cap U$. Therefore, after shrinking $U$, there exist a neighbourhood $V\subset U$ of $p$, an open one-sided neighbourhood $W\subset V\cap\Omega^-$ with $p\in\overline W$ and $M\cap V\subset\partial W$, and a function \begin{align*} F:W\to\mathbb C \end{align*} which is holomorphic on $W$, smooth up to $M\cap V$, and satisfies \begin{align*} F|_{M\cap V}=u|_{M\cap V}. \end{align*} [guided] The sign is the delicate point, so we keep the defining function fixed. We chose $\rho$ so that $\Omega^+\cap U=\{\rho>0\}$, and therefore the opposite side is \begin{align*} \Omega^-\cap U=\{z\in U:\rho(z)<0\}. \end{align*} The analytic input included in the theorem statement says that, for a defining function $r$ with a positive Levi eigenvalue at the base point, smooth CR functions extend to the side $\{r<0\}$. Here we take $r:=\rho$, so the target side in that input is exactly $\Omega^-\cap U$. We now verify every hypothesis of that input. The hypersurface $M$ is $C^\infty$ by assumption. The map $\rho:U\to\mathbb R$ is a $C^\infty$ local defining function and satisfies $d\rho_q\ne 0$ for every $q\in M\cap U$. The Levi form \begin{align*} \mathcal L_{\rho,p}:T^{1,0}_pM\times T^{1,0}_pM\to\mathbb C \end{align*} has a positive eigenvalue by hypothesis, meaning that some non-zero $L\in T^{1,0}_pM$ satisfies $\mathcal L_{\rho,p}(L,L)>0$ after diagonalising the Hermitian form. Define $T^{0,1}M:=\overline{T^{1,0}M}$. The condition $\bar\partial_bu=0$ means that every smooth local section of $T^{0,1}M$ annihilates $u$ on $M\cap U$, so $u\in C^\infty(M\cap U;\mathbb C)$ is a smooth CR boundary datum. The analytic input therefore supplies a neighbourhood $V\subset U$ of $p$, an [open set](/page/Open%20Set) $W\subset V\cap\Omega^-$ with $p\in\overline W$ and $M\cap V\subset\partial W$, and a map \begin{align*} F:W\to\mathbb C \end{align*} which is holomorphic on $W$, smooth up to $M\cap V$, and has trace \begin{align*} F|_{M\cap V}=u|_{M\cap V}. \end{align*} This proves the asserted one-sided extension, conditional on the stated Lewy analytic input. [/guided] [/step] [step:Recover the original CR function as the boundary value] The preceding step has already supplied a function $F:W\to\mathbb C$ that is holomorphic on $W$, smooth up to $M\cap V$, and satisfies \begin{align*} F|_{M\cap V}=u|_{M\cap V}. \end{align*} Since $W\subset V\cap\Omega^-$ and $M\cap V\subset\partial W$, this is a one-sided holomorphic extension to the side opposite the one on which $\rho$ is positive. This proves the stated conditional form of the Lewy extension principle. [/step]