abel-theorem: the CR-converse promotion (docs/design/abel-theorem.md §4.2 D2, §2.1 step 7)

Unit: abel-theorem. Namespace RS.Abel. Two deliverables:

• wirtingerDbar_exp_neg_mul_eq_zero — the dbarF = 0 computation underlying the meromorphic promotion: if u's Wirtinger dbar-derivative matches f's own logarithmic dbar-derivative (dbaru = dbarf / f) at a point where f ≠ 0, then F := exp(-u) * f has dbarF = 0 there — a direct Leibniz/chain-rule computation (wirtingerDbar_mul + the holomorphic-outer chain rule for Complex.exp, via mathlib's HasDerivAt.comp_hasFDerivAt).
• genus_eq_zero_of_exists_simple_pole_zero — Forster's necessity shortcut (§2.2): a meromorphic function with exactly one simple pole and one simple zero (elsewhere holomorphic and non-vanishing) forces genus X = 0, composing two ALREADY-BUILT, fully-proved facts (no admitted goals) — RS.homeoSphere_of_exists_simple_pole (proper-map-degree) and RS.SphereTopology.genus_eq_zero_of_homeo_sphere (sphere-topology). form-trace-tower is not imported anywhere in this unit, matching the design's finding (§2.2).

D2: the dbar-product-rule identity (mathlib-only, pure ℂ → ℂ)

theorem RS.Abel.wirtingerDbar_exp_neg_mul_eq_zero {u f : ℂ → ℂ} {z : ℂ} (hu : DifferentiableAt ℝ u z) (hf : DifferentiableAt ℝ f z) (h : wirtingerDbar u z = wirtingerDbar f z / f z) (hfz : f z ≠ 0) : wirtingerDbar (fun (w : ℂ) => Complex.exp (-u w) * f w) z = 0

D2, the dbarF = 0 computation (§2.1 step 7): the exponential-corrected function F := fun w => exp(-(u w)) * f w is genuinely dbar-flat wherever u's dbar-derivative matches f's own logarithmic one.

§2.2: Forster's necessity shortcut (via ALREADY-BUILT proper-map-degree/sphere-topology)

theorem RS.Abel.genus_eq_zero_of_exists_simple_pole {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (F : Mero X) (Q : X) (hpole : MeroGermOn.ord F Q = -1) (hreg : ∀ (x : X), x ≠ Q → 0 ≤ MeroGermOn.ord F x) : genus X = 0

The necessity shortcut this unit actually needs (§2.2): NOT Forster's general Trace(ω)-on-ℙ¹ necessity construction — just the "one simple pole" specialization, already fully discharged by two other units. form-trace-tower is not imported anywhere here.