residue-theorem: the general-X reduction and THE residue theorem

Unit: residue-theorem (docs/design/residue-theorem.md §6, primary route per the orchestrator addendum). This file closes Gap 2 of the previous partial delivery: the reduction of the general compact-connected case to the ℙ¹ base case (P1Assembly.lean) along a nonconstant map F := toP1 f' : X → ℙ¹, via form-trace-tower's resAtP1_trace_eq_sum fed with the CALIBRATED fiber stacks of Calibrated.lean.

Resolution of the convention mismatch flagged by the previous builder (d f vs resAtX's pullback convention at poles of f): no separate MForm.ofPullback object is needed. The two conventions differ exactly by the target-chart transition dz = -(w²)⁻¹ dw at the ∞ fibre, so the trace form is assembled from TWO coefficient functions of ONE pair (h', H∞), H∞ := -(f')²·h' (i.e. h · F^*(dz) re-expressed against F^*(dw)), matched fibre-by-fibre:

• resAtX_toP1_eq_of_ord_nonneg — over a finite value, resAtX F h' x = (h • d φ).resAt x;
• resAtX_toP1_eq_of_ord_neg — over ∞, resAtX F H∞ x = (h • d φ).resAt x;
• the ℙ¹-side coefficients glue into a single MFormData (OnePoint ℂ) via P1.formOfCoeFn because trace F H∞ = -(coeChart)²·(trace F h') away from ∞ (trace_const_mul_pullback + fibre-wise honesty of holoRepr).

Main exports:

• RS.residue_sum_eq_zero_of_exists_nonconstant — THE residue theorem ∑ᶠ x, θ.resAt x = 0 on a compact connected surface admitting a nonconstant meromorphic function (canonical-forms D9 exists_nonconstant_mero's exact export shape; now that Jacobian/CanonicalForms/Existence.lean has landed, the unconditional wrapper RS.residue_sum_eq_zero lives in Jacobian/ResidueTheorem/Unconditional.lean).
• RS.MForm.sum_resAt_eq_zero_of_exists_nonconstant — the serre-duality-tails consumption shape (docs/requests/residue-theorem.md): ∑ᶠ x, (f • θ).resAt x = 0.

RS.MForm.d_ne_zero moved to canonical-forms (Jacobian/CanonicalForms/Existence.lean): its proof used only canonical-forms/meromorphic-and-divisors machinery (no ℙ¹/trace/ calibration content), and canonical-forms itself needed exactly this fact for its own D9 existence chain (exists_ne_zero_mform := ⟨MForm.d f, MForm.d_ne_zero hf⟩). Since residue-theorem is DOWNSTREAM of canonical-forms, keeping a second copy here would either duplicate the ~90-line proof or require importing residue-theorem back into canonical-forms (a cycle); canonical-forms is the clean home, so this file now imports it from there instead (import Jacobian.CanonicalForms.Existence, above) — the call site below is unchanged.

Reading (h • d φ).resAt in the chart

Honesty of toP1 ∘ holoRepr at nonnegative-order points

The two bridging lemmas: resAtX against (h • d φ).resAt

theorem RS.resAtX_toP1_eq_of_ord_nonneg {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (φ h : Mero X) {x : X} (hx : 0 ≤ ordAtX (MeroGermOn.holoRepr φ) x) : FormTrace.resAtX (MTrace.toP1 (MeroGermOn.holoRepr φ)) (MeroGermOn.holoRepr h) x = (h • MForm.d φ).resAt x

Bridge, finite-value case: over a point where φ has nonnegative order (so F x = toP1 φ.holoRepr x is finite and the target chart is coeChart), the pair-form residue of h.holoRepr along F IS the residue of the 1-form h • d φ.

theorem RS.resAtX_toP1_eq_of_ord_neg {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (φ h : Mero X) {x : X} (hx : ordAtX (MeroGermOn.holoRepr φ) x < 0) : FormTrace.resAtX (MTrace.toP1 (MeroGermOn.holoRepr φ)) (fun (p : X) => -MeroGermOn.holoRepr φ p ^ 2 * MeroGermOn.holoRepr h p) x = (h • MForm.d φ).resAt x

Bridge, ∞-fibre case: over a pole of φ (so F x = ∞ and the target chart is invChart, i.e. the pullback convention reads against F^*(dw) with w = 1/z), the pair-form residue of the CORRECTED coefficient H∞ := -(φ.holoRepr)²·h.holoRepr along F is the residue of h • d φ — the dz = -(w²)⁻¹dw transition exactly cancels.

MForm.d_ne_zero — now imported from canonical-forms

Moved to Jacobian/CanonicalForms/Existence.lean (see the module docstring above): the proof never used any residue-theorem-specific content, and canonical-forms' own D9 existence chain needed exactly this fact. import Jacobian.CanonicalForms.Existence (above) brings it into scope unchanged; the call site below (MForm.d_ne_zero hφ) is untouched.

THE residue theorem

theorem RS.residue_sum_eq_zero_of_exists_nonconstant {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (hex : ∃ (f : Mero X), ∀ (c : ℂ), f ≠ (algebraMap ℂ (Mero X)) c) (θ : MForm X) : ∑ᶠ (x : X), θ.resAt x = 0

THE residue theorem (Forster 10.21 / Miranda VI eq. 3.2, blueprint headline ∑_p Res_p(θ) = 0): on a compact connected Riemann surface admitting a nonconstant meromorphic function (the exact shape of canonical-forms D9's exists_nonconstant_mero), the residues of any meromorphic 1-form sum to zero. The unconditional statement (hex discharged by exists_nonconstant_mero itself, now that Existence.lean has landed) is RS.residue_sum_eq_zero in Jacobian/ResidueTheorem/Unconditional.lean.

Proved by the trace route (design §6): write θ = h • d φ (D8, one-dimensionality over ℳ(X)), push down along F := toP1 φ.holoRepr fibre-by-fibre through calibrated fiber stacks (resAtP1_trace_eq_sum), assemble the trace data into a single meromorphic 1-form on ℙ¹ via formOfCoeFn, and conclude by the ℙ¹ base case (P1.sum_resAt_eq_zero).

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

The serre-duality-tails consumption shape (docs/requests/residue-theorem.md, sum_resAt_eq_zero): the residues of f • θ sum to zero, for any global meromorphic function f : ℳ X and meromorphic 1-form θ : MForm X. This is the well-definedness input of the Serre-pairing residue functional (RS.TailDuality.pairT_alpha, serre-duality-tails design §6 P3). Hypothesis-gated exactly like the main theorem; instantiate hex with canonical-forms D9's exists_nonconstant_mero once CanonicalForms/Existence.lean lands.

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

Finset-flexible corollary (the design §2 shape): the residues sum to zero over any finite set containing the support of resAt.