The argument principle (meromorphic-trace, cluster 1)

Unit: meromorphic-trace (docs/design/meromorphic-trace.md §2 D5, §4.3, §5 P3). Standing surface hypotheses throughout ([CompactSpace X] [ConnectedSpace X] load-bearing here, unlike files 1–2).

• finsum_ordAtX_eq_zero: for f meromorphic everywhere, "nonconstant" (toP1 f nonconstant), the (finite, junk-0-off-support) sum of orders of f on compact connected X is 0. THE argument principle — zeros counted with multiplicity cancel poles counted with multiplicity. Consumed by proper-map-degree for deg(divisor f) = 0.
• sum_ordAtX_eq_zero_of_finite: Finset-sum corollary (matches Divisor.degree's shape).
• finsum_ordAtX_eq_zero': convenience wrapper for callers holding the raw f-side nonconstancy hypothesis NotEventuallyConstX instead of toP1's.

Route (§0.4 of the design): via fiberMultSum_eq_degree at ↑0 and ∞ on ℙ¹ (mapping-degree's own well-definedness engine) — not via the residue theorem/Stokes (deliberately, per the design's routing warning; proper-map-degree needs the counting route, not a general-Stokes route).

theorem RS.MTrace.toP1_eq_coe_zero_iff_ordAtX_pos {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : X → ℂ} {x : X} (hf : MeromorphicOnX f Set.univ) : toP1 f x = ↑0 ↔ 0 < ordAtX f x

Translation lemma: toP1 f x = ↑0 iff f has a genuine zero at x (strictly positive order — excludes the "regular, nonvanishing" case ordAtX f x = 0, since an order-exactly-0 presentation has a nonzero limiting value, tendsto_ne_zero_of_meromorphicOrderAt_eq_zero).

theorem RS.MTrace.finsum_ordAtX_eq_zero {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {f : X → ℂ} (hf : MeromorphicOnX f Set.univ) (hne : ¬∃ (c : OnePoint ℂ), ∀ (x : X), toP1 f x = c) : ∑ᶠ (x : X), (ordAtX f x).untop₀ = 0

THE argument principle: the (finite, junk-0-off-support) sum of orders of a meromorphic, nonconstant function on a compact connected surface is 0. Consumed by proper-map-degree for deg(div f) = 0 (repackaging into Divisor/Divisor.degree terms is their bookkeeping).

theorem RS.MTrace.sum_ordAtX_eq_zero_of_finite {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {f : X → ℂ} {s : Finset X} (hf : MeromorphicOnX f Set.univ) (hne : ¬∃ (c : OnePoint ℂ), ∀ (x : X), toP1 f x = c) (hs : ∀ (x : X), ordAtX f x ≠ 0 → x ∈ s) : ∑ x ∈ s, (ordAtX f x).untop₀ = 0

Finset form (matches Divisor.degree's Finset.sum-over-finiteSupport shape) — a trivial corollary padding the finsum to any Finset containing the support.

theorem RS.MTrace.finsum_ordAtX_eq_zero' {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {f : X → ℂ} (hf : MeromorphicOnX f Set.univ) (hnc : NotEventuallyConstX f) : ∑ᶠ (x : X), (ordAtX f x).untop₀ = 0

Convenience packaging for callers holding the raw f-side nonconstancy hypothesis NotEventuallyConstX instead of toP1's (D3's translation, toP1_not_const).