Chain assembly (abel-weak-solutions, §7)

Unit: abel-weak-solutions (docs/design/abel-weak-solutions.md §7). Three deliverables:

• exists_weakSolutionOfFinset — the SCOPE ADDITION k-point layer (docs/design/abel-theorem.md §1.4/§4.1): assembled directly from SingleChart.exists_weakSolutionOfPair_chart (one call per index i, each pair already living inside its own chart neighbourhood — exactly what abel-theorem's own Thm 21.4(a) disjoint-chart construction sets up, per its design §1.4: "k pairwise disjoint two-point pieces, each already a Path (a i) (x i) living inside its own chart neighborhood") plus WeakSolution.isWeakSolutionOfFinset_prod.
• pathIntegral_eq_sum_chartChain (§7.2) — the CC6-compliant telescoped path-integral identity, pure Path-API bookkeeping (no Stokes).
• the Lemma-20.3-specialized residue identity (§7.3) — the harder, Stokes-driven half, via the two-puncture planar-stokes-atoms export RS.integral_wirtingerDbar_mul_inv_sub_sub_inv_sub_eq.

Status note on the general multi-chart exists_weakSolutionOfPair (design §6.3/§7.1, for an arbitrary path not confined to one chart): this file does NOT build it (only the disjoint-chart k-point layer above, and the telescoping/residue atoms). It is now built, in Rechart.lean + GeneralChain.lean (added by the abel-theorem builder, authorized to close this exact gap) — see the root file Jacobian/AbelWeak.lean for the full account: the missing piece was a "rechart" lemma for IsWeakSolutionAt (transporting a simple-zero/pole local model across a holomorphic chart transition via mathlib's removable-singularity theorem), plus a chain induction gluing SingleChart pieces at every interior breakpoint via a fully general order-additive IsWeakSolutionAt.mul.

The k-point layer (SCOPE ADDITION, abel-theorem's Thm 21.4(a)/(b) finding)

theorem RS.AbelWeak.exists_weakSolutionOfFinset {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {ι : Type u_2} [Finite ι] (a x : ι → X) (ha : Function.Injective a) (hx : Function.Injective x) (hax : ∀ (i j : ι), a i ≠ x j) {e : ι → OpenPartialHomeomorph X ℂ} (he : ∀ (i : ι), e i ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) (has : ∀ (i : ι), a i ∈ (e i).source) (hxs : ∀ (i : ι), x i ∈ (e i).source) {c : ι → ℂ} {ρ : ι → ℝ} (hρ : ∀ (i : ι), 0 < ρ i) (haQ : ∀ (i : ι), ↑(e i) (a i) - c i ∈ Metric.ball 0 (ρ i)) (haP : ∀ (i : ι), ↑(e i) (x i) - c i ∈ Metric.ball 0 (ρ i)) (ψ : ι → ContDiffBump 0) (hρψ : ∀ (i : ι), ρ i < (ψ i).rIn) (hballsub : ∀ (i : ι), Metric.closedBall (c i) (ψ i).rOut ⊆ (e i).target) : ∃ (f : X → ℂ) (U : Set X), IsWeakSolutionOfFinset f a x ∧ IsOpen U ∧ IsCompact (closure U) ∧ (∀ (i : ι), x i ∈ U) ∧ (∀ (i : ι), a i ∈ U) ∧ ∀ z ∉ U, f z = 1

Forster's Lemma 20.1, assembled: given k pairwise-disjoint pairs (x i, a i), each already living inside a common chart e i (matching the shape abel-theorem's own disjoint-chart 21.4(a) construction produces), there is a weak solution of the whole k-point configuration, equal to 1 outside a compact neighbourhood of the union of the per-pair chart balls.

§7.2: the telescoped path-integral identity (pure Path-API, no Stokes)

theorem RS.AbelWeak.pathIntegral_eq_sum_chartChain {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {x y : X} {γ : Path x y} (C : ChartChain γ) (η : Form1 X) (g : ℕ → ℂ → ℂ) (hg : ∀ k < C.n, ∀ z ∈ Metric.ball (C.c k) (C.r k), HasDerivAt (g k) (coeffIn (C.e k) η z) z) : pathIntegral γ η = ∑ k ∈ Finset.range C.n, (g k (↑(C.e k) (γ.extend (C.t (k + 1)))) - g k (↑(C.e k) (γ.extend (C.t k))))

The CC6-compliant replacement for Forster's ∫∫_X-formula (D5): for any ω : Form1 X and any ChartChain C adapted to γ, pathIntegral γ ω is exactly the finite telescoped sum of chart-local holomorphic-primitive differences.

§7.3: the Lemma-20.3-specialized residue identity (Stokes-driven)

theorem RS.AbelWeak.residue_identity_two_point {a b : ℂ} {U : Set ℂ} {g : ℂ → ℂ} (hU : IsOpen U) (hg : ContDiffOn ℝ 1 g U) (hcs : HasCompactSupport g) (hsub : tsupport g ⊆ U) : -1 / ↑Real.pi * ∫ (w : ℂ), wirtingerDbar g w * ((w - b)⁻¹ - (w - a)⁻¹) = g b - g a

Forster's Lemma 20.3, specialized to n = 2 (the residue identity abel-theorem needs to translate its period-vanishing hypothesis into a statement about a weak solution's chart-local log-derivative): for the two-puncture kernel (w - b)⁻¹ - (w - a)⁻¹ (residues +1 at b, -1 at a — matching a weak solution's own df/f local model, §7.3 step 3) and ANY C¹ compactly-supported g on an open U, the area integral of dbarg against that kernel recovers g b - g a, with no local-constancy hypothesis on g (the abel-weak-solutions refinement of planar-stokes-atoms' Atom 2 that this unit's design flagged as needed, §7.3/§10/§11 risk R1 — already supplied by planar-stokes-atoms' own RS.integral_wirtingerDbar_mul_inv_sub_sub_inv_sub_eq, cited directly here).

theorem RS.AbelWeak.logDeriv_rat_eq {a b z : ℂ} (hza : z ≠ a) (hzb : z ≠ b) : deriv (fun (w : ℂ) => (w - b) / (w - a)) z / ((z - b) / (z - a)) = (z - b)⁻¹ - (z - a)⁻¹

The two-puncture kernel (z - b)⁻¹ - (z - a)⁻¹ is EXACTLY the logarithmic derivative deriv h z / h z of the rational function h z := (z - b) / (z - a) (the inner-ball formula a SingleChart weak solution literally equals near its zero/pole pair) — connecting §7.3's abstract kernel to f's own chart-local log-derivative coefficient, as abel-theorem's translation step needs.