The planar log-branch atom (abel-weak-solutions, D2 / §6.1) #
Unit: abel-weak-solutions (docs/design/abel-weak-solutions.md §6.1). Pure ℂ → ℂ, no manifold
imports (matches Path/Planar.lean's hygiene). Two facts:
exists_logBranch_disk— the disk case: a holomorphic, non-vanishing function on a ball has a logarithm branch there (Complex.exp ∘ L = h), built from mathlib's disk-Morera primitive (DifferentiableOn.isExactOn_ball) plus a zero-derivative/uniqueness argument. No branch-cut case analysis onComplex.log/Complex.arganywhere. Spike-verified inscratch_abelweak.lean.exists_exteriorLogBranch— the exterior case Forster's construction actually needs: a log branch of(z - b)/(z - a)on{ρ < ‖z‖}fora, binsideball 0 ρ, obtained by transporting the disk case through the inversionw = 1/z(turning the exterior region into a genuine disk containing no singularity of the transported function at all — no winding-number/homotopy machinery needed).
theorem
RS.AbelWeak.exists_logBranch_disk
{c₀ : ℂ}
{r : ℝ}
(hr : 0 < r)
{h : ℂ → ℂ}
(hh : DifferentiableOn ℂ h (Metric.ball c₀ r))
(hne : ∀ z ∈ Metric.ball c₀ r, h z ≠ 0)
:
∃ (L : ℂ → ℂ),
(∀ z ∈ Metric.ball c₀ r, HasDerivAt L (deriv h z / h z) z) ∧ ∀ z ∈ Metric.ball c₀ r, Complex.exp (L z) = h z
The disk log-branch lemma (§6.1, disk case, spiked in scratch_abelweak.lean): a function
h differentiable and non-vanishing on ball c₀ r has a primitive L of h'/h there with
Complex.exp ∘ L = h on the ball.
theorem
RS.AbelWeak.exists_exteriorLogBranch
{a b : ℂ}
{ρ : ℝ}
(hρ : 0 < ρ)
(ha : a ∈ Metric.ball 0 ρ)
(hb : b ∈ Metric.ball 0 ρ)
:
The exterior log-branch lemma (§6.1, the engine Forster's construction actually needs): a
log branch of (z - b)/(z - a) on {ρ < ‖z‖} for a, b inside ball 0 ρ, via the substitution
w = 1/z turning the exterior region into a genuine disk ball 0 ρ⁻¹ containing no singularity
of the transported function H w := (1 - b*w)/(1 - a*w) at all.