genus (OnePoint ℂ) = 0 (CC5)

Unit: projective-line (docs/design/projective-line.md §3.5, proof plan P8). The coefficients of a holomorphic 1-form on ℙ¹, read in coeChart and invChart, are entire functions f, g related by f z = -(z ^ 2)⁻¹ * g z⁻¹ for z ≠ 0. Since g is bounded near 0 (continuity), f decays to 0 at infinity, hence vanishes identically by Liouville; the same transition rule then forces g ≡ 0. So there are no nonzero holomorphic 1-forms on ℙ¹ — the sphere has genus 0.

theorem RS.P1.form1_eq_zero (η : Form1 (OnePoint ℂ)) : η = 0

There are no nonzero holomorphic 1-forms on ℙ¹ (Forster 5-adjacent; "the sphere has genus 0").

instance RS.P1.instSubsingletonForm1OnePointComplex : Subsingleton (Form1 (OnePoint ℂ))

theorem RS.P1.finrank_form1 : Module.finrank ℂ (Form1 (OnePoint ℂ)) = 0

Module.finrank ℂ (RS.Form1 (OnePoint ℂ)) = 0, i.e. the space of holomorphic 1-forms on ℙ¹ is trivial.

theorem RS.genus_onePoint : genus (OnePoint ℂ) = 0

genus ℙ¹ = 0: the Riemann sphere has genus zero.