genus-zero-headline (#30): genus X = 0 ↔ X ≃ₜ S²

Unit: genus-zero-headline (clean_room_blueprint.md, docs/design/serre-duality-tails.md §9.1's "genus-0 single-simple-pole consequence" + docs/design/proper-map-degree.md's own consumer note). Assembles the two already-built halves:

• Backward (X ≃ₜ S² ⇒ genus X = 0): RS.SphereTopology.genus_eq_zero_of_homeo_sphere (sphere-topology, BUILT — pure topology: any space homeomorphic to the sphere is simply connected, hence has vanishing holomorphic 1-forms).
• Forward (genus X = 0 ⇒ X ≃ₜ S²): riemann-roch's riemann_inequality at D := single P 1 under genus X = 0 forces l(single P 1) ≥ 2 > 1 = l(0), so L(0) = span{1} is a PROPER subspace of L(single P 1) (SetLike.exists_of_lt, the CanonicalForms/Existence.lean pattern) — any witness φ outside L(0) has φ.ord ≥ -1 at P, φ.ord ≥ 0 elsewhere (mem_linSys_iff), and φ.ord P < 0 (else φ would be holomorphic everywhere, hence in L(0) = span{1} by linSys_zero_eq_span_one, contradiction); combined with φ.ord P ≥ -1 this forces φ.ord P = -1 exactly — a single simple pole, no other poles. proper-map-degree's already-built RS.homeoSphere_of_exists_simple_pole closes it.

Exports

• RS.GenusSphereHeadline.exists_simple_pole_of_genus_eq_zero — the forward-direction finisher.
• genus_eq_zero_iff_homeo (root level, docs/Jacobian_challenge.lean:54-56 verbatim, same standing variables — a direct alias target for final assembly).

theorem RS.GenusSphereHeadline.exists_simple_pole_of_genus_eq_zero {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] (hg : genus X = 0) : ∃ (φ : Mero X) (P : X), MeroGermOn.ord φ P = -1 ∧ ∀ (x : X), x ≠ P → 0 ≤ MeroGermOn.ord φ x

The forward-direction finisher: genus X = 0 produces a meromorphic function with exactly one simple pole (order -1 at some P) and no other poles (order ≥ 0 elsewhere) — RS.homeoSphere_of_exists_simple_pole's exact hypothesis shape.

theorem genus_eq_zero_iff_homeo {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : genus X = 0 ↔ Nonempty (X ≃ₜ ↑(Metric.sphere 0 1))

The headline (docs/Jacobian_challenge.lean:54-56, verbatim, standing variables): a compact Riemann surface has genus 0 iff it is homeomorphic to the sphere.