residue-theorem: the ℙ¹ base case, assembled

Unit: residue-theorem (docs/design/residue-theorem.md §6). This file closes Gap 1 of the previous partial delivery (see RationalOnP1.lean's module docstring): the headline

• RS.P1.sum_resAt_eq_zero : ∑ᶠ y, Θ.resAt y = 0 for every Θ : MForm (OnePoint ℂ).

The junk-value blocker documented in RationalOnP1.lean ("the remainder R_mid, built by bare pointwise subtraction of MeromorphicAt-junk-valued functions, has order ≥ 0 at the former poles but need not be continuous there") is repaired via mathlib's meromorphic normal form machinery rather than a weakened contour radius:

• RS.P1.exists_differentiable_of_ord_nonneg — a planar function meromorphic on all of ℂ with everywhere-nonnegative order admits an ENTIRE representative agreeing with it at every point where it is honestly analytic (toMeromorphicNFOn, which only changes values on the non-normal-form set).

The proof of the headline follows the design: subtract the finite principal-part tail at the (finitely many, via the divisor) finite poles, repair the remainder to an entire Rf, kill the remainder's residue at ∞ by the Liouville-free contour fact (resAt_neg_sq_inv_mul_comp_inv_eq_zero), and compute the tail's companion residue at ∞ as -∑ (finite residues) by the monomial computation (resAt_neg_sq_inv_mul_sub_inv_zpow). The key honesty input making the ∞-chart congruences legitimate for a RAW representative is coeffAt_infty_eq (the two-chart compat identity, valid POINTWISE on ℂ \ {0}), which also forces R to be honestly analytic near ∞.

The normal-form repair

theorem RS.P1.exists_differentiable_of_ord_nonneg {g : ℂ → ℂ} (hg : MeromorphicOn g Set.univ) (hord : ∀ (z : ℂ), 0 ≤ meromorphicOrderAt g z) : ∃ (gf : ℂ → ℂ), Differentiable ℂ gf ∧ (∀ (z : ℂ), AnalyticAt ℂ g z → gf z = g z) ∧ ∀ (z : ℂ), gf =ᶠ[nhdsWithin z {z}ᶜ] g

Repair lemma: a function meromorphic on all of ℂ with everywhere-nonnegative order admits an entire representative that agrees with it wherever it is honestly analytic (and in particular on a punctured neighborhood of every point).

The two-chart compatibility identity, pointwise

theorem RS.P1.coeffAt_infty_eq (θ : MFormData (OnePoint ℂ)) {z : ℂ} (hz : z ≠ 0) : θ.coeffAt OnePoint.infty z = -(z ^ 2)⁻¹ * θ.coeffAt (↑0) z⁻¹

The ∞-chart coefficient of any raw 1-form on ℙ¹ is the transition-rule image of the shared finite-chart coefficient — POINTWISE on ℂ \ {0} (this is compat itself, not a germ statement, so it survives junk values).

THE ℙ¹ base case

theorem RS.P1.sum_resAt_eq_zero (Θ : MForm (OnePoint ℂ)) : ∑ᶠ (y : OnePoint ℂ), Θ.resAt y = 0

The residue theorem on ℙ¹ (the genus-0 base case of the residue theorem, task item 2): the residues of any meromorphic 1-form on the projective line sum to zero.