abel-theorem: the weak-solution-upgrade discharge (design §4.1 steps 5-7, assembled)

Unit: abel-theorem. Namespace RS.Abel.

The discharge of WeakSolutionUpgrade/WeakSolutionUpgradeFinset modulo the single serre-duality-tails gate. The core (exists_mero_of_sum_pathIntegral_eq_zero): given finitely many paths δ i : Path (A i) (B i) whose TOTAL integral against every holomorphic 1-form vanishes, there is a global meromorphic F with ord_z F = ∑ i ([z = B i] - [z = A i]).

Proof shape (Forster 20.5/20.7(a), dissection-free):

• chop each path by RS.exists_chartChain; build one exists_link piece per chain link (LinkData.lean), giving piece functions f_l and packaged (0,1)-forms η_l;
• pairing PU (∑ η_l) θ = π ∑ᵢ ∫_{δ i} θ = 0 — per link the residue identity evaluates the pairing at chart primitives, and pathIntegral_eq_sum_chartChain telescopes them back into the path integrals (the SAME primitives, from DifferentiableOn.isExactOn_ball);
• the Serre-functional bridge exists_dbar_of_forall_pairing_eq_zero (gated on Function.Surjective (tailToH1 0)) yields u with dbaru = ∑ η_l;
• F₀ := exp (-u) · ∏ f_l is dbar-closed off the divisor points (wirtingerDbar_exp_neg_mul_eq_zero + the per-link dbar log-matching + the dbar product rule), hence holomorphic there (contMDiffOn_omega_of_isDbarOn_zero), and the per-link factor limits multiply into the promotion lemma meromorphicAt_of_tendsto_factor at EVERY point — meromorphy plus the exact order ∑ linkOrd in one stroke, no rechart bookkeeping.

Consumers: weakSolutionUpgrade_of_surjective and weakSolutionUpgradeFinset_of_surjective — design §4.1 steps 5-7 discharged, gated ONLY on serre-duality-tails's single remaining external fact (the same gate as DolbeaultBridge.lean; the weak-solution hypotheses of the WeakSolutionUpgrade shapes are simply not needed: the construction builds its own pieces).

Small algebra helpers

theorem RS.Abel.pairing_zero_left {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (PU : SurfPoU X) (θ : Form1 X) : pairing PU 0 θ = 0

theorem RS.Abel.pairing_finsetSum_left {X : Type u_1} [TopologicalSpace X] [CompactSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (PU : SurfPoU X) {ι : Type u_2} (s : Finset ι) (F : ι → Form01 X) (θ : Form1 X) : pairing PU (∑ i ∈ s, F i) θ = ∑ i ∈ s, pairing PU (F i) θ

theorem RS.Abel.zpow_finset_sum {ι : Type u_2} {a : ℂ} (ha : a ≠ 0) (s : Finset ι) (f : ι → ℤ) : a ^ ∑ i ∈ s, f i = ∏ i ∈ s, a ^ f i

theorem RS.Abel.contMDiffAt_mul_real' {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {f g : X → ℂ} {x : X} (hf : ContMDiffAt (modelWithCornersSelf ℝ ℂ) (modelWithCornersSelf ℝ ℂ) (↑⊤) f x) (hg : ContMDiffAt (modelWithCornersSelf ℝ ℂ) (modelWithCornersSelf ℝ ℂ) (↑⊤) g x) : ContMDiffAt (modelWithCornersSelf ℝ ℂ) (modelWithCornersSelf ℝ ℂ) (↑⊤) (fun (y : X) => f y * g y) x

Real-smooth multiplication on the surface, through the preferred chart (no ContMDiffMul 𝓘(ℝ, ℂ) ∞ ℂ instance exists — the AbelWeak compat route).

The core discharge

theorem RS.Abel.exists_mero_of_sum_pathIntegral_eq_zero {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {ι : Type u_2} [Fintype ι] [ConnectedSpace X] [DecidableEq X] (hsurj : Function.Surjective ⇑(LaurentTail.tailToH1 0)) {A B : ι → X} (δ : (i : ι) → Path (A i) (B i)) (hper : ∀ (θ : Form1 X), ∑ i : ι, pathIntegral (δ i) θ = 0) : ∃ (F : Mero X), F ≠ 0 ∧ ∀ (z : X), MeroGermOn.ord F z = ↑(∑ i : ι, linkOrd (A i) (B i) z)

The Abel sufficiency engine (Forster 20.5 + 20.7(a), assembled; gated only on serre-duality-tails's remaining external fact): finitely many paths with vanishing total period produce a global meromorphic function whose divisor is exactly the endpoint divisor.

The gated discharges of the two isolated hypotheses

theorem RS.Abel.weakSolutionUpgrade_of_surjective {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [ConnectedSpace X] [DecidableEq X] (hsurj : Function.Surjective ⇑(LaurentTail.tailToH1 0)) : WeakSolutionUpgrade X

Design §4.1 steps 5-7, DISCHARGED modulo serre-duality-tails's single remaining external fact: WeakSolutionUpgrade X holds. (The weak-solution argument of the hypothesis is not needed — the construction builds its own chain pieces along the given zero-period path.)

theorem RS.Abel.weakSolutionUpgradeFinset_of_surjective {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [ConnectedSpace X] [DecidableEq X] {ι : Type u_2} [Fintype ι] (hsurj : Function.Surjective ⇑(LaurentTail.tailToH1 0)) : WeakSolutionUpgradeFinset X ι

The k-point discharge (design §4.1, the shape period-lattice-rank's Thm 21.4(b) consumes), same single gate.