Complex points with $uv\ne0$ are Zariski dense in the chart curve of $P_\alpha=0$ at $(\infty,\infty)$

Let $m\ge1$ be an integer and let $\alpha\in\mathbb C$ be arbitrary. Let $P_\alpha(X,Y)=X^m(\alpha+XY)+Y^m(\bar\alpha+XY)$ and $R_\alpha(u,v)=u^m+v^m+uv\,(\bar\alpha u^m+\alpha v^m)\in\mathbb C[u,v]$. For $uv\ne0$ one has $R_\alpha(u,v)=u^{m+1}v^{m+1}P_\alpha(1/u,1/v)$, so $R_\alpha$ is the equation of the curve $P_\alpha=0$ in the chart $u=1/X$, $v=1/Y$ around the point $(\infty,\infty)$ of $\mathbb P^1\times\mathbb P^1$. For $w\in\mathbb C^2$ let $\mathfrak m_w$ be the maximal ideal of the polynomials vanishing at $w$, a point of $\operatorname{Spec}\mathbb C[u,v]$, and let $V(R_\alpha)$ be the set of prime ideals containing $R_\alpha$.

Then, in the Zariski topology of $\operatorname{Spec}\mathbb C[u,v]$,

Neither irreducibility nor smoothness of the curve $R_\alpha=0$ is assumed, and $\alpha$ may be real. The points with $w_0w_1\ne0$ correspond to the points $(1/w_0,1/w_1)$ of the affine curve $P_\alpha=0$ with $XY\ne0$, so the whole chart curve lies in the closure of the affine curve. The formalization uses this when the four standard charts are glued, to show that the zero set of the bihomogeneous equation lies in the closure of the curve (6) in $\mathbb P^1\times\mathbb P^1$.

Formalization Note: points of $\operatorname{Spec}\mathbb C[u,v]$ are elements of PrimeSpectrum (MvPolynomial (Fin 2) ℂ) with Mathlib's Zariski topology, $u$ and $v$ are the variables X 0 and X 1, and $\mathfrak m_w$ is the kernel of evaluation at $w$.