The genus-0 engine: simply connected ⇒ every Form1 has a global primitive (CC-sphere-topology)

Unit: sphere-topology (docs/design/sphere-topology.md §3). Forster 10.5: on a simply connected compact surface, every holomorphic 1-form is exact (indeed zero, since a global primitive is a holomorphic function on a compact connected surface, hence constant). The "engine" atom (contMDiff_and_mdifferential_eq_of_isPrimitiveAlongMap_id) is shared, in spirit, with the monodromy unit's discrete-continuation route (see module docstring of docs/design/ sphere-topology.md §3.1 for the reuse note) — monodromy is free to reuse it verbatim or re-derive it.

Main declarations:

• RS.SphereTopology.contMDiff_and_mdifferential_eq_of_isPrimitiveAlongMap_id — a primitive of η along the identity map is a genuine holomorphic global primitive with mdifferential = η.
• RS.SphereTopology.exists_isPrimitiveAlongMap_id — construction of the global primitive on a simply connected X, via pathIntegral from a fixed base point.
• RS.SphereTopology.form1_eq_zero_of_simplyConnectedSpace, the Subsingleton (Form1 X) instance, and the headline RS.SphereTopology.genus_eq_zero_of_simplyConnectedSpace.

theorem RS.SphereTopology.contMDiff_and_mdifferential_eq_of_isPrimitiveAlongMap_id {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {η : Form1 X} {F : X → ℂ} (hF : IsPrimitiveAlongMap id η F Set.univ) : ∃ (hF' : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F), mdifferential F hF' = η

The "monodromy engine" atom: a primitive of η along the identity map is a genuine holomorphic global primitive, and it IS η's antiderivative in Forms' sense.

theorem RS.SphereTopology.exists_isPrimitiveAlongMap_id {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [SimplyConnectedSpace X] (x₀ : X) (η : Form1 X) : ∃ (F : X → ℂ), IsPrimitiveAlongMap id η F Set.univ ∧ F x₀ = 0

Construction of the global primitive on a simply connected X, via pathIntegral from a fixed base point (well-defined by pathIntegral_eq_of_simplyConnected).

theorem RS.SphereTopology.form1_eq_zero_of_simplyConnectedSpace {X : Type u_1} [TopologicalSpace X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [SimplyConnectedSpace X] (η : Form1 X) : η = 0

Forster 10.5. On a simply connected compact surface every holomorphic 1-form vanishes.

instance RS.SphereTopology.instSubsingletonForm1OfSimplyConnectedSpace {X : Type u_1} [TopologicalSpace X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [SimplyConnectedSpace X] : Subsingleton (Form1 X)

theorem RS.SphereTopology.genus_eq_zero_of_simplyConnectedSpace {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [SimplyConnectedSpace X] : genus X = 0

The step-2 headline.