The single-chart weak solution (abel-weak-solutions, §6.2-6.3)

Unit: abel-weak-solutions (docs/design/abel-weak-solutions.md §6.2-6.3). Given two distinct points P, Q lying inside a common chart e, both within ball c ρ for some c, ρ, and a ContDiffBump (0 : ℂ) cutoff ψ with ρ < ψ.rIn, closedBall c ψ.rOut ⊆ e.target: builds a weak solution of the pair (P, Q), equal to 1 outside the compact set e.symm '' closedBall c ψ.rOut.

The construction (exists_weakSolutionOfPair_chart): the planar function g z := if ‖z - c‖ ≤ ρ then (z - e P) / (z - e Q) else exp(ψ(z - c) * L(z - c)), where L is the exterior log-branch (PlanarLogBranch.exists_exteriorLogBranch) of (z-eP)/(z-eQ) recentred at c. The bump's one_of_mem_closedBall/zero_of_le_dist make g interpolate exactly from the rational function (near c) to the constant 1 (far from c), with no matching argument beyond Set.EqOn-rewriting on the transition annulus (the same shape the design's §6.2 step 1 describes).

theorem RS.AbelWeak.exists_weakSolutionOfPair_chart {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] {P Q : X} (hPQ : P ≠ Q) {e : OpenPartialHomeomorph X ℂ} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) (hPs : P ∈ e.source) (hQs : Q ∈ e.source) {c : ℂ} {ρ : ℝ} (hρ : 0 < ρ) (haQ : ↑e Q - c ∈ Metric.ball 0 ρ) (haP : ↑e P - c ∈ Metric.ball 0 ρ) (ψ : ContDiffBump 0) (hρψ : ρ < ψ.rIn) (hballsub : Metric.closedBall c ψ.rOut ⊆ e.target) : ∃ (f : X → ℂ), IsWeakSolutionOfPair f P Q ∧ IsOpen (↑e.symm '' Metric.ball c ψ.rOut) ∧ IsCompact (closure (↑e.symm '' Metric.ball c ψ.rOut)) ∧ P ∈ ↑e.symm '' Metric.ball c ψ.rOut ∧ Q ∈ ↑e.symm '' Metric.ball c ψ.rOut ∧ ∀ x ∉ ↑e.symm '' Metric.ball c ψ.rOut, f x = 1

The single-chart weak solution (§6.2-6.3).