deg(div φ) = 0 and the unconditional L(D) = 0 for negative degree (proper-map-degree, file 2

of 3)

Unit: proper-map-degree (docs/design/proper-map-degree.md §3.2). The argument principle, repackaged from MeromorphicTrace's ℂ-valued statement (RS.MTrace.finsum_ordAtX_eq_zero', Jacobian/MeromorphicTrace/ArgumentPrinciple.lean) into ℳ X/Divisor vocabulary, plus the unconditional discharge of Meromorphic/LinearSystem.lean's conditional linSys_eq_bot_of_degree_neg.

Design-doc update: at design time MeromorphicTrace/ArgumentPrinciple.lean had not yet landed, so the design's §3.2 proof plan was a ~110–150 line self-contained re-derivation of the zeros-equal-poles finsum identity (§5 R1's documented fallback). By build time ArgumentPrinciple.lean HAD landed (finsum_ordAtX_eq_zero/sum_ordAtX_eq_zero_of_finite/ finsum_ordAtX_eq_zero', all complete with zero admitted gaps), so per the design's own adapter note this file uses the "cite instead of reprove" short route: divisor_degree_eq_zero's only remaining work is (a) the constancy case split translating ℳ X-nonconstancy to MTrace.NotEventuallyConstX, and (b) matching Divisor.degree's Finset-sum shape to the finsum via Function.locallyFinsuppWithin.degree_eq_sum_of_subset (Meromorphic/Divisor.lean) — both purely mechanical, no new mathematical content. ~60 lines total, well under the design's own "if landed" estimate of 40–60 lines (the extra margin is the constancy-translation case split).

• RS.divisor_degree_eq_zero — THE argument principle in Divisor/ℳ X terms.
• RS.sum_ord_eq_zero_of_finite — Finset padding corollary.
• RS.linSys_eq_bot_of_degree_neg' — the unconditional discharge of Meromorphic/LinearSystem.lean:206's conditional linSys_eq_bot_of_degree_neg (primed since the unprimed name is already taken in the same RS namespace by that file — cannot rename their declaration, CONVENTIONS.md rule 4).

theorem RS.divisor_degree_eq_zero {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (φ : Mero X) (hφ : φ ≠ 0) : Function.locallyFinsuppWithin.degree (divisor φ) = 0

deg(div φ) = 0 for nonzero φ : ℳ X — the argument principle, repackaged from MeromorphicTrace's built finsum_ordAtX_eq_zero' into Divisor/CC2 terms. Consumed by serre-duality-tails/riemann-roch (mainly via linSys_eq_bot_of_degree_neg' below).

theorem RS.sum_ord_eq_zero_of_finite {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {φ : Mero X} (hφ : φ ≠ 0) {s : Finset X} (hs : Function.locallyFinsuppWithin.support (divisor φ) ⊆ ↑s) : ∑ x ∈ s, (divisor φ) x = 0

Finset padding corollary (matches Divisor.degree's definitional Finset shape).

theorem RS.linSys_eq_bot_of_degree_neg' {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (D : Divisor X) (h : Function.locallyFinsuppWithin.degree D < 0) : LinSys D = ⊥

The unconditional discharge of Meromorphic.linSys_eq_bot_of_degree_neg's hdeg hypothesis — the whole point of routing deg(div f)=0 through this unit.