abel-theorem: the per-link construction (design §4.1 steps 5-7, link layer)

Unit: abel-theorem. Namespace RS.Abel.

exists_link lifts one planar LogPieceData into a chart of the surface: given two points A (pole) and B (zero) inside a common chart ball — exactly what one ChartChain link supplies — it produces the piece function f : X → ℂ (the SingleChart.lean recipe: g ∘ e on the chart source, 1 outside) TOGETHER with its packaged global (0,1)-form η = dbar log f (via ChartSupportedData.form) and the five facts the assembly (UpgradeDischarge.lean) needs:

1. real-smoothness off the pole;
2. non-vanishing off the divisor;
3. the dbar log-matching dbar(f ∘ chart⁻¹) = η-coefficient · f at every preferred-chart center off the divisor;
4. the punctured-limit factorization f(z)·(z - z₀)^(-linkOrd) → C ≠ 0 at EVERY point (the Rechart-free order bookkeeping input);
5. the pairing identity ∫∫ η ∧ θ = π (Gp(eB) - Gp(eA)) for any chart primitive Gp of θ (pairing_form + integral_dlog_mul).

Also here: the planar promotion lemma meromorphicAt_of_tendsto_factor (punctured holomorphy plus a factor limit pin meromorphicOrderAt, via mathlib's removable-singularity theorem and tendsto_ne_zero_iff_meromorphicOrderAt_eq_zero) and the dbar finite product rule wirtingerDbar_finset_prod.

The planar promotion lemma

theorem RS.Abel.meromorphicAt_of_tendsto_factor {F : ℂ → ℂ} {z₀ C : ℂ} {m : ℤ} {V : Set ℂ} (hV : V ∈ nhds z₀) (hF : DifferentiableOn ℂ F (V \ {z₀})) (hC : C ≠ 0) (h : Filter.Tendsto (fun (z : ℂ) => F z * (z - z₀) ^ (-m)) (nhdsWithin z₀ {z₀}ᶜ) (nhds C)) : MeromorphicAt F z₀ ∧ meromorphicOrderAt F z₀ = ↑m

Promotion: punctured holomorphy near z₀ plus the factor limit F(z)(z-z₀)^{-m} → C ≠ 0 force F meromorphic at z₀ of order exactly m.

The dbar finite product rule

theorem RS.Abel.differentiableAt_finset_prod {ι : Type u_1} (s : Finset ι) {f : ι → ℂ → ℂ} {z : ℂ} (hf : ∀ i ∈ s, DifferentiableAt ℝ (f i) z) : DifferentiableAt ℝ (fun (w : ℂ) => ∏ i ∈ s, f i w) z

theorem RS.Abel.wirtingerDbar_finset_prod {ι : Type u_1} [DecidableEq ι] (s : Finset ι) {f : ι → ℂ → ℂ} {z : ℂ} (hf : ∀ i ∈ s, DifferentiableAt ℝ (f i) z) : wirtingerDbar (fun (w : ℂ) => ∏ i ∈ s, f i w) z = ∑ i ∈ s, wirtingerDbar (f i) z * ∏ j ∈ s.erase i, f j z

The link order and the per-link construction

def RS.Abel.linkOrd {X : Type u_1} [DecidableEq X] (A B x : X) : ℤ

The contribution of the link (A ↦ pole, B ↦ zero) to the order at x.

Equations

• RS.Abel.linkOrd A B x = (if x = B then 1 else 0) - if x = A then 1 else 0

theorem RS.Abel.linkOrd_self_eq_zero {X : Type u_1} [DecidableEq X] (A x : X) : linkOrd A A x = 0

theorem RS.Abel.exists_link {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [DecidableEq X] {A B : X} {e : OpenPartialHomeomorph X ℂ} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) (hA : A ∈ e.source) (hB : B ∈ e.source) {c : ℂ} {r : ℝ} (hball : Metric.ball c r ⊆ e.target) (hAm : ↑e A ∈ Metric.ball c r) (hBm : ↑e B ∈ Metric.ball c r) : ∃ (f : X → ℂ) (η : Form01 X), ContMDiffOn (modelWithCornersSelf ℝ ℂ) (modelWithCornersSelf ℝ ℂ) (↑⊤) f {A}ᶜ ∧ (∀ (x : X), x ≠ A → x ≠ B → f x ≠ 0) ∧ (∀ (x : X), x ≠ A → x ≠ B → wirtingerDbar (f ∘ ↑(chartAt ℂ x).symm) (↑(chartAt ℂ x) x) = η.coeffAt x (↑(chartAt ℂ x) x) * f x) ∧ (∀ (x : X), ∃ (C : ℂ), C ≠ 0 ∧ Filter.Tendsto (fun (z : ℂ) => f (↑(chartAt ℂ x).symm z) * (z - ↑(chartAt ℂ x) x) ^ (-linkOrd A B x)) (nhdsWithin (↑(chartAt ℂ x) x) {↑(chartAt ℂ x) x}ᶜ) (nhds C)) ∧ ∀ (PU : SurfPoU X) (θ : Form1 X) (Gp : ℂ → ℂ), (∀ z ∈ Metric.ball c r, HasDerivAt Gp (coeffIn e θ z) z) → pairing PU η θ = ↑Real.pi * (Gp (↑e B) - Gp (↑e A))

The link construction (design §4.1 step 5, one chain link): the piece function f, its packaged (0,1)-form η, and the five assembly facts. Degenerate links (A = B) yield the constant 1 and the zero form.