The sphere, embedded by $p\mapsto(p,\bar p)$, meets $V_\alpha$ exactly in the spherical closure $\widehat C_{m,\alpha}$

Let $m\ge 1$ be an integer and let $\alpha\in\mathbb C$ with $\alpha\ne\bar\alpha$, that is, $\alpha\notin\mathbb R$; no condition on $|\alpha|$ is imposed. Let $C_{m,\alpha}=\{z\in\mathbb C:\operatorname{Re}\bigl(z^m(|z|^2+\alpha)\bigr)=0\}$ and let $\widehat C_{m,\alpha}$ be its closure in the Riemann sphere $\widehat{\mathbb C}=\mathbb C\cup\{\infty\}$. Complex conjugation $p\mapsto\bar p$ acts on $\widehat{\mathbb C}$, with $\bar\infty=\infty$.

Identify $\widehat{\mathbb C}$ with the complex projective line $\mathbb P^1$ by $\iota(z)=[z:1]$ for $z\in\mathbb C$ and $\iota(\infty)=[1:0]$. For $x=(x_0,x_1)$ and $y=(y_0,y_1)$ in $\mathbb C^2$ let

the bihomogeneous form of bidegree $(m+1,m+1)$ with $F_\alpha\bigl((X,1),(Y,1)\bigr)=P_\alpha(X,Y)=X^m(\alpha+XY)+Y^m(\bar\alpha+XY)$, and let $V_\alpha=\{([x],[y])\in\mathbb P^1\times\mathbb P^1:F_\alpha(x,y)=0\}$ be its zero set.

Then for every $p\in\widehat{\mathbb C}$

The note complexifies the plane curve by $X=z$, $Y=\bar z$ and considers the closure $V_\alpha$ of the curve $P_\alpha=0$ of equation (6) in $\mathbb P^1\times\mathbb P^1$, which is given by the bihomogeneous equation above. This result says that the sphere, embedded in $\mathbb P^1\times\mathbb P^1$ by $p\mapsto(p,\bar p)$, meets $V_\alpha$ exactly in $\widehat C_{m,\alpha}$, the point at infinity included. The formalization uses it to pass between Möbius maps of the sphere and the induced maps of $\mathbb P^1\times\mathbb P^1$, as in the proof of Theorem 2.

Formalization Note: the sphere is OnePoint ℂ, $\mathbb P^1$ is Projectivization ℂ (Fin 2 → ℂ) and $\iota$ is Mathlib's OnePoint.equivProjectivization. $V_\alpha$ is defined as the zero set of $F_\alpha$ evaluated on chosen representatives, which is harmless because $F_\alpha$ is bihomogeneous, and $\widehat C_{m,\alpha}$ is the topological closure in OnePoint ℂ.