TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-26

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Every contour missing a point admits a continuous logarithm, unique up to a constant in $2 π i Z$

Statement

Let $γ : [a, b] \to C$ be a complex contour and let $p \in C$ with $p \notin γ^{*}$ . Then:

there is a continuous logarithm $λ$ of $γ - p$ along $γ$ (Continuous logarithms and continuous arguments along a contour);
if $λ_{1}$ and $λ_{2}$ are two of them, then $λ_{1} - λ_{2}$ is a constant function with value in $2 π i Z$ ;
for each $v \in C$ with $\exp v = γ (a) - p$ there is exactly one continuous logarithm $λ$ of $γ - p$ along $γ$ with $λ (a) = v$ .

In particular the increment $λ (b) - λ (a)$ , and the increment $θ (b) - θ (a)$ of the associated continuous argument, are the same for every choice of $λ$ . No differentiability of $γ$ is used.

Facts & Assumptions

Given: A complex contour $γ : [a, b] \to C$ and a point $p \notin γ^{*}$ .

[L1]

A continuous logarithm of $γ - p$ along $γ$ is a continuous $λ : [a, b] \to C$ with $\exp (λ (t)) = γ (t) - p$ for every $t$ ; a holomorphic logarithm branch of $z - p$ on an open $V$ missing $p$ is a holomorphic $L$ on $V$ with $\exp (L (z)) = z - p$ (Continuous logarithms and continuous arguments along a contour).

[L2]

For a complex contour $γ$ and $p \notin γ^{*}$ , the distance $d = \inf {∣ w - p ∣ : w \in γ^{*}}$ is positive and there is $δ > 0$ such that every partition $a = t_{0} < \dots < t_{r} = b$ of mesh below $δ$ has $γ ([t_{i}, t_{i + 1}]) \subseteq D (γ (t_{i}), d)$ and $p \notin D (γ (t_{i}), d)$ for every $i < r$ ; at least one such partition exists (A contour missing a point subdivides into arcs lying in discs that miss it).

[L3]

If $D (c, ρ)$ is an open disc with $ρ > 0$ and $p \notin D (c, ρ)$ , there is a holomorphic $L$ on $D (c, ρ)$ with $\exp (L (z)) = z - p$ there (A disc missing $p$ carries a holomorphic logarithm of $z - p$ ).

[L4]

$\ker (\exp) = 2 π i Z$ , and $\exp z = \exp w$ exactly when $z - w \in 2 π i Z$ ( $\ker (\exp) = 2 π i Z$ , and $\exp z = \exp w$ exactly when $z - w \in 2 π i Z$ ).

[L5]

The complex exponential maps $C$ onto $C ∖ {0}$ (The complex exponential maps $C$ onto $C ∖ {0}$ ).

[L6]

$\exp (z + w) = \exp z \exp w$ for all $z, w \in C$ ( $\exp (z + w) = \exp z \exp w$ , and the complex exponential extends the real exponential).

[L7]

The continuous image of a connected subset is a connected subset (A continuous image of a connected space is connected, and connectedness is a topological property).

[L8]

A subset $E \subseteq R$ is connected exactly when it is order-convex (The connected subspaces of $R$ with its usual topology are exactly the order-convex subsets, the published characterisation transported by the identification of the two descriptions of "open in $R$ "); a closed bounded interval is order-convex (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).

[L9]

If a property holds at $0$ and passes from $n$ to $n + 1$ , it holds for every natural number (The principle of mathematical induction).

[L10]

A composite of continuous maps is continuous, and a function whose restrictions to the members of a finite closed cover are continuous is continuous (Continuity may be checked on any open cover, and on any finite closed cover; composites of continuous maps are continuous).

[L11]

For $z = a + b i$ with $a, b$ real, $Im z = b$ and $∣ z ∣ = \sqrt{a^{2} + b^{2}}$ (Real and imaginary parts, complex conjugation, and modulus).

[L12]

A function complex differentiable at a point is continuous there (Complex differentiability at a point implies continuity there).

[L13]

The integers form an ordered commutative ring, and their canonical image in $R$ is discrete; hence if $m < n$ then $m + \frac{1}{2}$ lies strictly between them and is not an integer (The integers form a commutative ring, The integers form a totally ordered ring, Integer part: for every real $x$ there is exactly one integer $m$ with $m \leq x < m + 1$ ).

Proof

technique · direct

1.1

Since $p \notin γ^{*}$ , the number $γ (a) - p$ is nonzero, so [L5] supplies $v \in C$ with $\exp v = γ (a) - p$ ; more generally, for every such $v$ the set of complex numbers with that exponential is $v + 2 π i Z$ by [L4].

givenL4L5

1.2

If $λ_{1}, λ_{2}$ are continuous logarithms of $γ - p$ along $γ$ , then $\exp (λ_{1} (t)) = \exp (λ_{2} (t))$ for every $t$ , so $λ_{1} (t) - λ_{2} (t) \in 2 π i Z$ by [L4]; the real-valued function $g = Im (λ_{1} - λ_{2}) / (2 π)$ is continuous by [L10] and [L11] and takes values in $Z$ , so by [L7] and [L8] its image is an order-convex subset of $R$ inside $Z$ , which by [L13] can only be a single point. Hence $λ_{1} - λ_{2}$ is a constant in $2 π i Z$ , and it is $0$ when $λ_{1} (a) = λ_{2} (a)$ .

L1L4L7L8L10L11L13

1.3

Assume $a < b$ . By [L2] there are $d > 0$ and a partition $a = t_{0} < t_{1} < \dots < t_{r} = b$ with $γ ([t_{i}, t_{i + 1}]) \subseteq D_{i} : = D (γ (t_{i}), d)$ and $p \notin D_{i}$ for every $i < r$ .

givenL2

2.1

By [L3] each $D_{i}$ carries a holomorphic $L_{i}$ with $\exp (L_{i} (z)) = z - p$ for $z \in D_{i}$ , and $L_{i}$ is continuous on $D_{i}$ by [L12].

step 1.3L3L12

2.2

Define $c_{0} : = v$ and, for each $i < r$ , define $c_{i + 1} : = c_{i} + L_{i} (γ (t_{i + 1})) - L_{i} (γ (t_{i}))$ ; this determines the finite list $c_{0}, \dots, c_{r}$ . Now define $λ$ on $[t_{i}, t_{i + 1}]$ by $λ (t) = c_{i} + L_{i} (γ (t)) - L_{i} (γ (t_{i}))$ . The two formulas available at a shared point $t_{i}$ with $0 < i < r$ agree, the $i$ th giving $c_{i}$ and the $(i - 1)$ st giving $c_{i - 1} + L_{i - 1} (γ (t_{i})) - L_{i - 1} (γ (t_{i - 1})) = c_{i}$ , so $λ : [a, b] \to C$ is a well-defined function with $λ (a) = v$ and $λ (t_{i}) = c_{i}$ for every $i \leq r$ .

step 1.1step 1.3

3.1

Each restriction $λ ∣_{[t_{i}, t_{i + 1}]}$ is continuous, being a constant plus the composite of $γ$ with $L_{i}$ of step 2.1; the intervals $[t_{i}, t_{i + 1}]$ form a finite closed cover of $[a, b]$ , so $λ$ is continuous by [L10].

step 2.1step 2.2L10

3.2

For every $i < r$ and $t \in [t_{i}, t_{i + 1}]$ , [L6] gives $\exp (λ (t)) = \exp (c_{i}) \exp (L_{i} (γ (t))) \exp (L_{i} (γ (t_{i})))^{- 1}$ , and $\exp (L_{i} (γ (t))) = γ (t) - p$ by step 2.1, so $\exp (c_{i}) = γ (t_{i}) - p$ forces $\exp (λ (t)) = γ (t) - p$ and, at $t = t_{i + 1}$ , $\exp (c_{i + 1}) = γ (t_{i + 1}) - p$ . Since $\exp (c_{0}) = \exp (v) = γ (a) - p$ , an induction on $i$ ([L9]) gives $\exp (λ (t)) = γ (t) - p$ for every $t \in [a, b]$ .

step 1.1step 2.1step 2.2L6L9

4.1

Steps 3.1 and 3.2 make $λ$ a continuous logarithm of $γ - p$ along $γ$ with $λ (a) = v$ , which proves claims 1 and 3 when $a < b$ ; when $a = b$ the constant function with value $v$ does the same, since its only value satisfies $\exp v = γ (a) - p$ . Claim 2 is step 1.2, which also gives the uniqueness in claim 3, and it makes $λ (b) - λ (a)$ and its imaginary part independent of the choice by [L1] and [L11].

step 1.2step 3.1step 3.2L1L11∎

Depends on

Used by

Cited to discharge well-definedness by Continuous logarithms and continuous arguments along a contour.

Dependency tree · two levels

105 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

L. V. Ahlfors, Complex Analysis, 3rd ed., Ch. 4 §2.1, Exercise 2 (standard reference, not scraped)
J. Lebl, Complex Analysis, Ch. 4 §4.1 (standard reference, not scraped)

Every contour missing a point admits a continuous logarithm, unique up to a constant in 2πiZ2πiZ