The unconditional residue theorem (D9 gate now open)

Unit: residue-theorem (docs/design/residue-theorem.md). Reduction.lean's residue_sum_eq_zero_of_exists_nonconstant/MForm.sum_resAt_eq_zero_of_exists_nonconstant/ residueTheorem_of_exists_nonconstant were stated against the hypothesis hex : ∃ f : ℳ X, ∀ c, f ≠ algebraMap ℂ (ℳ X) c — EXACTLY canonical-forms D9's exists_nonconstant_mero shape — because Jacobian/CanonicalForms/Existence.lean had not yet landed. It now has (its own gate, Jacobian/Finiteness/Chi.lean, closed), so every conditional export here becomes unconditional by discharging hex with RS.exists_nonconstant_mero — each a one-line corollary.

Exports

• RS.residue_sum_eq_zero (θ : MForm X) : ∑ᶠ x, θ.resAt x = 0 — THE residue theorem, unconditional.
• RS.MForm.sum_resAt_eq_zero (f : ℳ X) (θ : MForm X) : ∑ᶠ x, (f • θ).resAt x = 0 — the tail-duality consumption shape (docs/requests/residue-theorem.md), unconditional; this is the name serre-duality-tails' pairT_alpha well-definedness argument should thread instead of MForm.sum_resAt_eq_zero_of_exists_nonconstant now that no hypothesis needs to be supplied.
• RS.residueTheorem (θ : MForm X) {S : Finset X} (hS : ...) : ∑ x ∈ S, θ.resAt x = 0 — the Finset-flexible unconditional corollary.

theorem RS.residue_sum_eq_zero {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (θ : MForm X) : ∑ᶠ (x : X), θ.resAt x = 0

THE residue theorem, unconditional (Forster 10.21 / Miranda VI eq. 3.2): on ANY compact connected Riemann surface, the residues of a meromorphic 1-form sum to zero. Existence of the nonconstant meromorphic function the trace-route proof needs is no longer a hypothesis — D9 (exists_nonconstant_mero) supplies it unconditionally.

theorem RS.MForm.sum_resAt_eq_zero {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (f : Mero X) (θ : MForm X) : ∑ᶠ (x : X), (f • θ).resAt x = 0

The tail-duality consumption shape, unconditional: the residues of f • θ sum to zero for any global meromorphic function f and meromorphic 1-form θ.

theorem RS.residueTheorem {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (θ : MForm X) {S : Finset X} (hS : (Function.support fun (x : X) => θ.resAt x) ⊆ ↑S) : ∑ x ∈ S, θ.resAt x = 0

Finset-flexible unconditional corollary: the residues sum to zero over any finite set containing the support of resAt.