The holomorphic differentials of $w^2=-t(t^m+1)(\alpha t^m+\bar\alpha)$ are spanned by $t^i\,dt/w$, $0\le i<m$

Let $m\ge1$ be an integer and $\alpha\in\mathbb C$ with $\alpha\ne\bar\alpha$. Put $h_\alpha(t)=-t(t^m+1)(\alpha t^m+\bar\alpha)\in\mathbb C[t]$ and let $K_\alpha=\mathbb C(t)[W]/(W^2-h_\alpha(t))$, with $w$ the class of $W$, so that $w^2=h_\alpha(t)$; this is the function field of the double cover of the $t$-line in equation (7) of the note, written with $w=t(t^m+1)Y$. Let $\Omega_{K_\alpha/\mathbb C}$ be its module of Kähler differentials, with universal derivation $d$. For a point $(t_0,w_0)\in\mathbb C^2$ of the affine curve $w^2=h_\alpha(t)$, that is, with $w_0^2=h_\alpha(t_0)$, let $\mathcal O_{(t_0,w_0)}\subset K_\alpha$ be its local ring: the localization of $\mathbb C[t][W]/(W^2-h_\alpha)$ at the maximal ideal of $(t_0,w_0)$, viewed inside $K_\alpha$.

For the conjugate parameter, $K_{\bar\alpha}$ is built in the same way, with coordinate $s$ and root $w'$, where $w'^2=h_{\bar\alpha}(s)=-s(s^m+1)(\bar\alpha s^m+\alpha)$. Since $h_{\bar\alpha}(0)=0$, the point $(0,0)$ lies on the curve $w'^2=h_{\bar\alpha}(s)$; let $\mathcal O'_{(0,0)}\subset K_{\bar\alpha}$ be its local ring there. Let $\Phi\colon K_\alpha\to K_{\bar\alpha}$ be the isomorphism of $\mathbb C$-algebras with $\Phi(t)=1/s$ and $\Phi(w)=w'\,s^{-(m+1)}$ (the chart at $t=\infty$), and let $\Phi_\ast\colon\Omega_{K_\alpha/\mathbb C}\to\Omega_{K_{\bar\alpha}/\mathbb C}$ be the induced map, $\Phi_\ast(g\,dk)=\Phi(g)\,d\Phi(k)$.

A differential $\omega\in\Omega_{K_\alpha/\mathbb C}$ is regular at a point $(t_0,w_0)$ if $f\in\mathcal O_{(t_0,w_0)}$ whenever $u\in\mathcal O_{(t_0,w_0)}$ generates the maximal ideal of $\mathcal O_{(t_0,w_0)}$ and $\omega=f\,du$ with $f\in K_\alpha$. It is regular at infinity if $\Phi_\ast\omega$ is regular, in the same sense, at the point $(0,0)$ of $w'^2=h_{\bar\alpha}(s)$. It is holomorphic if it is regular at every point $(t_0,w_0)$ of $w^2=h_\alpha(t)$ and at infinity. The holomorphic differentials form a complex vector subspace $\mathcal H_\alpha\subseteq\Omega_{K_\alpha/\mathbb C}$.

Then

With the linear independence of these $m$ differentials, they form a basis of $\mathcal H_\alpha$. This explicit basis, rather than the Riemann–Hurwitz count used in the note's proof, is how the formalization obtains the genus $m$ in Lemma 4.

Formalization Note: the hypotheses $m>0$ and $\alpha\ne\bar\alpha$ are Fact instances; $|\alpha|=1$ is not assumed.