SimplyConnectedSpace (OnePoint ℂ) (CC-sphere-topology, design §2)

Unit: sphere-topology (docs/design/sphere-topology.md §2). No van Kampen: OnePoint ℂ's two polar caps {∞}ᶜ/{↑0}ᶜ are each homeomorphic to ℂ (hence simply connected), and the paths-and-integrals unit's loop-perturbation lemma RS.Loop.exists_homotopic_avoiding pushes any based loop off whichever of ∞/↑0 is NOT its basepoint, landing it inside one of the two simply connected caps.

Note on RS.Loop.exists_homotopic_avoiding: this file was written and compiled against that lemma's stated signature while Jacobian/Path/Perturb.lean still carried one documented placeholder step upstream (the general multi-chart induction, design risk R4 of paths-and-integrals). That placeholder has since been resolved upstream (see docs/build-log.md, "Perturb.lean FIXED"), so this file now consumes a fully proved lemma; nothing here needed to change.

Main declarations:

• RS.SphereTopology.isSimplyConnected_compl_infty/isSimplyConnected_compl_coeZero.
• instance : PathConnectedSpace (OnePoint ℂ).
• RS.SphereTopology.simplyConnectedSpace_onePoint (the headline instance).
• RS.SphereTopology.simplyConnectedSpace_of_homeoOnePoint (homeomorphism transfer).
• RS.SphereTopology.simplyConnectedSpace_sphere (the challenge sphere model).

theorem RS.SphereTopology.isSimplyConnected_compl_infty : IsSimplyConnected {OnePoint.infty}ᶜ

Both "polar caps" of the two-chart atlas are simply connected: they are each homeomorphic to ℂ (contractible), via the open embedding (↑) : ℂ → OnePoint ℂ for {∞}ᶜ.

theorem RS.SphereTopology.isSimplyConnected_compl_coeZero : IsSimplyConnected {↑0}ᶜ

The other polar cap, {↑0}ᶜ, is simply connected too (feeds the x = ∞ case of the basepoint split), via inversionHomeomorph swapping ∞ ↔ ↑0.

instance RS.SphereTopology.instPathConnectedSpaceOnePointComplex_leanPool : PathConnectedSpace (OnePoint ℂ)

OnePoint ℂ is path connected (local path-connectedness transports through the two-chart atlas from ℂ's local convexity, combined with the existing ConnectedSpace instance).

instance RS.SphereTopology.simplyConnectedSpace_onePoint : SimplyConnectedSpace (OnePoint ℂ)

The headline of this file: no van Kampen, no universal cover — assembled from the perturbation lemma + the two polar-cap facts above.

theorem RS.SphereTopology.simplyConnectedSpace_of_homeoOnePoint {X : Type u_1} [TopologicalSpace X] (e : X ≃ₜ OnePoint ℂ) : SimplyConnectedSpace X

Homeomorphism transfer (generic; consumed by Headline.lean and anything producing X ≃ₜ OnePoint ℂ).

instance RS.SphereTopology.simplyConnectedSpace_sphere : SimplyConnectedSpace ↑(Metric.sphere 0 1)

Same fact stated for the literal challenge sphere type, for convenience/reuse.