homeoSphere_of_exists_simple_pole (proper-map-degree, file 3 of 3)

Unit: proper-map-degree (docs/design/proper-map-degree.md §3.3). The meromorphic-function version of degree-1 ⇒ homeomorphism: a single simple pole (no other poles) forces the induced ℙ¹-valued map RS.MTrace.toP1 f to have degree exactly 1, hence X ≃ₜ ℙ¹ ≃ₜ S². This is genus-zero-headline's forward-headline finisher: the caller (riemann-roch's genus-0 single-simple-pole existence result) supplies φ and the pole location Q, nothing else. φ ≠ 0/nonconstancy of φ are derived, not required — φ.ord Q = -1 alone already rules out both. This file has zero dependency on MeromorphicTrace/ArgumentPrinciple.lean (unlike DivisorDegreeZero.lean): the nonconstancy witness here is the explicit pole location Q itself, cheaper than the general codiscrete-nonconstancy argument.

Main declaration: RS.homeoSphere_of_exists_simple_pole.

theorem RS.homeoSphere_of_exists_simple_pole {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (φ : Mero X) (Q : X) (hpole : MeroGermOn.ord φ Q = -1) (hreg : ∀ (x : X), x ≠ Q → 0 ≤ MeroGermOn.ord φ x) : Nonempty (X ≃ₜ ↑(Metric.sphere 0 1))

The meromorphic-function version of degree-1 ⇒ homeomorphism: a single simple pole (no other poles) forces the induced ℙ¹-valued map to have degree exactly 1, hence X is homeomorphic to ℙ¹, hence to S². Consumed by genus-zero-headline's forward direction.