residue-theorem: the ℙ¹ base case — atoms (file 1/1, PARTIAL DELIVERY)

Unit: residue-theorem (docs/design/residue-theorem.md §6, docs/design/form-trace-tower.md §RationalOnP1). Target headline: ∑ᶠ p, θ.resAt p = 0 for θ : MForm (OnePoint ℂ), as the genus-0 base case feeding the general-X reduction via a nonconstant map to ℙ¹ (design §6).

Status: the headline theorem is NOT proved here — read this note before building on this file. What follows is a complete (no open goals anywhere), independently useful collection of atoms toward it, plus an honest account of the one remaining gap and how to close it. See Jacobian/ ResidueTheorem.lean (unit root) for the full write-up of what is/isn't delivered and why.

What IS built, zero sorries

• RS.P1.formOfCoeFn: packages an arbitrary meromorphic "coefficient in the finite chart" function R : ℂ → ℂ into a genuine MFormData (OnePoint ℂ), given that its invChart-transported reading fun w => -(w²)⁻¹ * R w⁻¹ is also meromorphic. The two-chart compat check reduces to "apply the transition rule twice returns to the start", independent of what R is.
• RS.P1.coeffAt_coe_eq_coeffAt_coe: any MFormData (OnePoint ℂ)'s finite-chart coefficient is the same raw function at every finite basepoint (all of ℙ¹'s finite points share coeChart).
• The Liouville-free residue-at-infinity fact (RS.P1.circleIntegral_inv_eq_neg + RS.P1.resAt_neg_sq_inv_mul_comp_inv_eq_zero): for R_mid differentiable on all of ℂ, the residue "at infinity" of its invChart reading vanishes — via Cauchy's theorem (an entire function's circle integral is 0 at every radius) transported through the z ↦ z⁻¹ reindexing of the contour, NOT a polynomial-growth/degree argument. This is the "Liouville" ingredient the task brief anticipated, done more cheaply than the growth-bound route the non-quotient form-trace-tower design had budgeted for.
• RS.P1.meromorphicAt_neg_sq_inv_mul_sub_inv_zpow / RS.P1.resAt_neg_sq_inv_mul_sub_inv_zpow: the "companion pole at ∞" bookkeeping for a single principal-part monomial (w⁻¹ - a) ^ k (k < 0) — meromorphic at 0, with residue -1 for the simple pole k = -1 (Miranda's "dz/(z-a) has residues 1 at a and -1 at ∞") and 0 otherwise.

What is NOT built: the assembly, and why (read before attempting it)

The intended proof: extract θ's finite-chart coefficient R, subtract the finite sum of its principal parts at its finitely many finite poles (RS.principalPartAt, already built) to get a remainder R_mid, apply the Liouville-free fact above to conclude the remainder's residue at ∞ vanishes, then telescope (the tail's own residue at ∞ is exactly minus the sum of residues it reproduces at the finite poles it was built to match, by resAt_neg_sq_inv_mul_sub_inv_zpow).

The blocker, found late and not resolved in the time available: resAt_neg_sq_inv_mul_comp_inv_eq_zero needs R_mid genuinely Differentiable ℂ — but R_mid := R - R_tail is built from MeromorphicAt data, whose junk convention at a pole/removable point does not force the value there to match the analytic-repair limit (MeromorphicAt f x with witness order n > 0 puts no constraint on f x at all, since it is multiplied by (x - x) ^ n = 0). So R_mid, built by bare pointwise subtraction, may fail to be continuous at the finitely many points of θ's pole set even though its order is ≥ 0 there (checked and proved separately, via MeromorphicAt.orderAt_sub_ principalPartAt_nonneg + a Finset.analyticAt_fun_sum argument — that part of the assembly DID work, it is only the final "hence Differentiable ℂ, hence apply the Liouville-free fact" step that does not follow as stated). Two fixes, either workable, neither attempted: (a) weaken resAt_neg_sq_inv_mul_comp_inv_eq_zero to take an explicit radius R₀ with R_mid differentiable only on closedBall 0 R₀ \ {0} for R₀ small enough to exclude the (finite) pole set — the circle-integral argument only ever needs one such disk, and resAt at 0 doesn't care which; or (b) repair R_mid first (canonical-forms' MeroGermOn.holoRepr-style construction, already used elsewhere in this project, e.g. MForm.d) to an honestly continuous representative before invoking Cauchy's theorem. Route (a) is probably the smaller patch — the Set.Finite/Metric "there is a positive radius smaller than the nearest nonzero pole" lemma is routine, and every other piece of the assembly (the finite-pole-sum construction, the order-≥0 argument, the θ.coeffAt ∞ transition formula, the finite pole set extraction from θ.divisor) was fully worked out and test-compiled during this build and is recorded in this design's build notes for the next attempt; none of it is included here as code because it was written against the now-known-insufficient Differentiable ℂ R_mid hypothesis and would need re-threading through whichever fix is chosen.

theorem RS.P1.chartAt_target_eq_univ (x : OnePoint ℂ) : (chartAt ℂ x).target = Set.univ

chartAt's target is univ at every point of ℙ¹ (both charts have target univ).

noncomputable def RS.P1.formOfCoeFn (R : ℂ → ℂ) (hR : MeromorphicOn R Set.univ) (hR' : MeromorphicOn (fun (w : ℂ) => -(w ^ 2)⁻¹ * R w⁻¹) Set.univ) : MFormData (OnePoint ℂ)

The chart-coefficient family assembled from a "finite-chart" function R, forced to be a genuine MFormData (OnePoint ℂ) by requiring its invChart reading (the transition-rule image) to also be meromorphic. The two-chart compat check is a single "apply the transition rule twice returns to the start" computation, independent of what R is.

Equations

• RS.P1.formOfCoeFn R hR hR' = { coeffAt := fun (x : OnePoint ℂ) (z : ℂ) => x.elim (-(z ^ 2)⁻¹ * R z⁻¹) fun (x : ℂ) => R z, coeffAt_zero_off := ⋯, meromorphicOn_coeffAt := ⋯, compat := ⋯ }

theorem RS.P1.coeffAt_coe_eq_coeffAt_coe (θ : MFormData (OnePoint ℂ)) (a b : ℂ) : θ.coeffAt ↑a = θ.coeffAt ↑b

The coeChart reading of an MFormData (OnePoint ℂ) is the same function for every finite basepoint (ℙ¹'s finite points all share the identical coeChart, and compat with the identity transition forces literal equality of the raw functions, not just a germ agreement).

The Liouville-free "residue at infinity of an entire function vanishes" fact

theorem RS.P1.circleIntegral_inv_eq_neg (R_mid : ℂ → ℂ) {ρ : ℝ} (hρ : 0 < ρ) : ∮ (w : ℂ) in C(0, ρ), -(w ^ 2)⁻¹ * R_mid w⁻¹ = -∮ (z : ℂ) in C(0, ρ⁻¹), R_mid z

Circle integral under z ↦ z⁻¹ reindexing: reading the same integrand through the inversion at reciprocal radius reverses orientation (a -1 sign), the classical "residue at infinity" substitution, via circleMap_zero_inv + a period-shift of the parametrizing integral.

theorem RS.P1.resAt_neg_sq_inv_mul_comp_inv_eq_zero {R_mid : ℂ → ℂ} (hdiff : Differentiable ℂ R_mid) (hg : MeromorphicAt (fun (w : ℂ) => -(w ^ 2)⁻¹ * R_mid w⁻¹) 0) : resAt (fun (w : ℂ) => -(w ^ 2)⁻¹ * R_mid w⁻¹) 0 = 0

The Liouville-free key fact. The residue "at infinity" (i.e. the residue at 0 of the invChart-transported reading -(w²)⁻¹ R_mid w⁻¹) of an ENTIRE R_mid always vanishes: Cauchy's theorem gives R_mid's own circle integral 0 at every radius, and circleIntegral_inv_eq_neg transports this to the transported reading's circle integral at every (reciprocal) radius, hence its residue is 0. No polynomial-growth/degree bookkeeping needed anywhere.

The finite-pole/z⁻¹ compatibility of principalPartAt's monomials

theorem RS.P1.meromorphicAt_neg_sq_inv_mul_sub_inv_zpow (a : ℂ) (k : ℤ) : MeromorphicAt (fun (w : ℂ) => -(w ^ 2)⁻¹ * (w⁻¹ - a) ^ k) 0

Each monomial (w⁻¹ - a) ^ k composed with the inversion, weighted by the dz ↦ dw factor -(w²)⁻¹, is meromorphic at 0 (the "companion pole at ∞" bookkeeping): the closed form -(1 - a w) ^ k * w ^ (-k - 2) shows it directly, for any a : ℂ, k : ℤ.

theorem RS.P1.resAt_neg_sq_inv_mul_sub_inv_zpow (a : ℂ) {k : ℤ} (hk : k < 0) : resAt (fun (w : ℂ) => -(w ^ 2)⁻¹ * (w⁻¹ - a) ^ k) 0 = if k = -1 then -1 else 0

The residue at 0 of the transported monomial -(w²)⁻¹ (w⁻¹ - a) ^ k, for k < 0 (the only exponents RS.principalPartAt ever produces): -1 for the simple pole k = -1 (the "companion at ∞"), 0 otherwise — the elementary case split.