The general multi-chart exists_weakSolutionOfPair

Unit: abel-weak-solutions, closing the gap recorded in this unit's own root docstring and in docs/design/abel-theorem.md §1.4/§4.1. Builds the fully general two-point weak solution for an ARBITRARY connecting path (not confined to one chart), by inducting along a RS.ChartChain and gluing adjacent SingleChart pieces via Rechart.lean's IsWeakSolutionAt.mul.

The induction, in one paragraph

Given δ : Path Q P, obtain a ChartChain δ (C) and set M k := δ.extend (C.t k) (the breakpoints, M 0 = Q, M C.n = P). By induction on m, build f_m agreeing with the eventual answer's local model at M 0 (order ordAt m (M 0) ∈ {-1, 0}) and at the CURRENT endpoint M m (order ordAt m (M m) ∈ {0, 1}), smooth away from M 0, nonvanishing away from {M 0, M m}, and = 1 outside a compact-closure open set U_m ∋ M 0. The step m → m + 1: if M (m+1) = M m the piece is degenerate (nothing to do); otherwise get a fresh SingleChart weak solution g of the pair (M (m+1), M m) inside the chain's own m-th chart-ball (shrunk via three nested midpoint radii so SingleChart's bump-function hypotheses fit inside the chart's target), and glue f_m and g via IsWeakSolutionAt.mul at every point where either has nonzero order — this is at most THREE points (M 0, M m, M (m+1), with the possible coincidences M 0 = M m or M 0 = M (m+1) handled by 3 exhaustive cases, chainFinishSame/chainFinish doing the bookkeeping). At m = C.n the invariant is exactly IsWeakSolutionOfPair f P Q; Q ∈ U is tracked throughout (seeded by a small chart-ball B0 ∋ M 0 at the base case) and P ∈ U follows by contradiction (a weak solution of nonzero order genuinely vanishes at its own point, contradicting the = 1 off-U value if P ∉ U).

Small helpers

theorem RS.AbelWeak.IsWeakSolutionAt.congr_of_eventuallyEq {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f g : X → ℂ} {a : X} {k : ℤ} (hf : IsWeakSolutionAt f a k) (hfg : f =ᶠ[nhds a] g) : IsWeakSolutionAt g a k

IsWeakSolutionAt transports along eventual equality of the underlying function.

theorem RS.AbelWeak.IsWeakSolutionAt.apply_eq_zero_of_ne_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : X → ℂ} {a : X} {k : ℤ} (hf : IsWeakSolutionAt f a k) (hk : k ≠ 0) : f a = 0

A weak solution of NONZERO order genuinely vanishes at its own point (a pole is assigned the junk value 0 there too, by the zpow-at-zero convention; a zero vanishes for real).

theorem RS.AbelWeak.isWeakSolutionAt_one_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (a : X) : IsWeakSolutionAt (fun (x : X) => 1) a 0

The constant function 1 is (trivially) a weak solution of order 0 at any point.

theorem RS.AbelWeak.isWeakSolutionAt_zero_of_ne {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {f : X → ℂ} {p q x : X} (hcm : ContMDiffOn (modelWithCornersSelf ℝ ℂ) (modelWithCornersSelf ℝ ℂ) (↑⊤) f {p}ᶜ) (hne : ∀ (y : X), y ≠ p → y ≠ q → f y ≠ 0) (hxp : x ≠ p) (hxq : x ≠ q) : IsWeakSolutionAt f x 0

A function that is ContMDiffOn away from p and nonvanishing away from {p, q} is, at any OTHER point x ∉ {p, q}, a weak solution of order 0 (smooth, nonvanishing — no genuine zero or pole there).

theorem RS.AbelWeak.IsWeakSolutionAt.contMDiffAt_and_ne_zero_of_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : X → ℂ} {a : X} (hf : IsWeakSolutionAt f a 0) : ContMDiffAt (modelWithCornersSelf ℝ ℂ) (modelWithCornersSelf ℝ ℂ) (↑⊤) f a ∧ f a ≠ 0

Converse of isWeakSolutionAt_zero_of_ne's conclusion: order 0 at a unfolds to genuine smoothness and nonvanishing there.

theorem RS.AbelWeak.IsWeakSolutionAt.contMDiffAt_of_nonneg {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {f : X → ℂ} {a : X} {k : ℤ} (hf : IsWeakSolutionAt f a k) (hk : 0 ≤ k) : ContMDiffAt (modelWithCornersSelf ℝ ℂ) (modelWithCornersSelf ℝ ℂ) (↑⊤) f a

A nonnegative order (k ≥ 0, i.e. a genuine zero, k > 0, or the order-0 case) unfolds to genuine smoothness (no ≠ 0 conclusion — a zero really does vanish there).

The general chain induction

theorem RS.AbelWeak.exists_weakSolutionOfPair {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {P Q : X} (hPQ : Q ≠ P) (δ : Path Q P) : ∃ (f : X → ℂ) (U : Set X), IsWeakSolutionOfPair f P Q ∧ IsOpen U ∧ IsCompact (closure U) ∧ P ∈ U ∧ Q ∈ U ∧ ∀ x ∉ U, f x = 1

The general multi-chart weak solution (§6.3/§7.1 of abel-weak-solutions.md, the gap this file closes): for an ARBITRARY path δ : Path Q P (not confined to one chart), there is a weak solution of the pair (P, Q). Built by inducting along a RS.ChartChain δ (Jacobian.Path.Chain), gluing one SingleChart piece per chain link via IsWeakSolutionAt.mul (Rechart.lean) — the +1-order zero of one piece cancels the -1-order pole of the next at every interior breakpoint, including the (rare, but real) case where the breakpoint recurs at the chain's own basepoint Q.