CorollaryStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 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.

The principal logarithm is the normalised holomorphic branch on the slit plane

Statement

Let $S = C ∖ {x \in R : x \leq 0}$ be the slit plane. Then $S$ is a complex domain, star-shaped with respect to $1$ , and homologically simply connected. The principal logarithm $Log$ (Complex logarithms, the principal logarithm, and principal and multivalued complex powers) is the unique holomorphic $F : S \to C$ with

$\exp (F (z)) = z (z \in S) and F (1) = 0,$

and it satisfies ${Log}^{'} (z) = 1 / z$ on $S$ .

Facts & Assumptions

Given: The slit plane $S = C ∖ {x \in R : x \leq 0}$ ; segments and star-shapedness in the plane are those of Complex star-shaped and convex domains are the published Euclidean notions under the identification $C = R^{2}$ .

[L1]

On a homologically simply connected complex domain, a holomorphic nowhere-zero $f$ admits a holomorphic $L$ with $\exp \circ L = f$ , and any two such differ by a constant in $2 π i Z$ (A nonvanishing holomorphic function on a homologically simply connected domain has a holomorphic logarithm).

[L2]

A nonempty open star-shaped subset of $C$ is a complex domain and is homologically simply connected (Star-shaped plane domains are homologically simply connected).

[L3]

If $L$ and $h$ are holomorphic on an open set with $\exp \circ L = h$ , then $h$ is nowhere zero and $L^{'} = h^{'} / h$ (A holomorphic logarithm is a primitive of the logarithmic derivative).

[L4]

For $z \neq 0$ with principal polar form $z = r (\cos θ + i \sin θ)$ and $- π < θ \leq π$ , $Log z = \log r + i θ$ (Complex logarithms, the principal logarithm, and principal and multivalued complex powers).

[L5]

Every $z \neq 0$ has a unique representation $z = r (\cos θ + i \sin θ)$ with $r = ∣ z ∣ > 0$ and $- π < θ \leq π$ (Every nonzero complex number has a unique polar form $r (\cos θ + i \sin θ)$ with $r > 0$ and $- π < θ \leq π$ ).

[L6]

For $z \neq 0$ the solutions of $\exp w = z$ are exactly $Log z + 2 π i k$ for $k \in Z$ (All logarithms of $z \neq 0$ are $Log z + 2 π i k$ , $k \in Z$ ).

[L7]

For real $x, y$ , $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ and $∣ \exp (x + i y) ∣ = e^{x}$ ( $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ ).

[L8]

A continuous real function on $[a, b]$ attains every value between $f (a)$ and $f (b)$ (Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on $[a, b]$ takes every value between $f (a)$ and $f (b)$ ).

[L9]

A nonempty open $U \subseteq R^{n}$ is star-shaped with respect to $a \in U$ when $a + t (x - a) \in U$ for every $x \in U$ and $0 \leq t \leq 1$ (Star-shaped open subsets of Euclidean space).

[L10]

A complex domain is a nonempty, connected, open subset of $C$ (A complex domain is a nonempty connected open subset of $C$ ).

[L11]

For $x > 0$ , $\log x$ is the unique real $y$ with $\exp y = x$ (The natural logarithm as the inverse of the exponential function).

[L12]

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

[L13]

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

[L14]

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

[L15]

A set is open exactly when each of its points admits a ball inside it (The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement, Open ball, closed ball and sphere in a metric space).

[L16]

$Z$ is the ring of integers (The integers as equivalence classes of pairs of naturals).

Proof

technique · direct

1.1

$S$ is open: if $z = x + i y \in S$ with $y \neq 0$ then the ball of radius $∣ y ∣$ about $z$ contains no real number, and if $y = 0$ then $x > 0$ and the ball of radius $x$ about $z$ contains no real number $\leq 0$ ; in both cases [L14] and [L15] put a ball around $z$ inside $S$ . It is nonempty, since $1 \in S$ .

givenL14L15

1.2

$S$ is star-shaped with respect to $1$ in the sense of [L9]: for $z \in S$ and $0 \leq t \leq 1$ put $w = 1 + t (z - 1)$ . If $w$ were a real number $\leq 0$ then $Im w = t Im z = 0$ by [L14]; $t = 0$ gives $w = 1 > 0$ , so $t > 0$ and $Im z = 0$ , making $z$ a real number, necessarily $z > 0$ because $z \in S$ ; but then $w = (1 - t) + t z > 0$ , a contradiction.

givenL9L14

2.1

By steps 1.1 and 1.2 and [L2], $S$ is a complex domain and is homologically simply connected.

step 1.1step 1.2L2L10

3.1

The identity function $h (z) = z$ is holomorphic and nowhere zero on $S$ , because $0 \notin S$ , so [L1] gives a holomorphic $G$ on $S$ with $\exp \circ G = h$ ; since $\exp (G (1)) = 1$ , [L12] puts $G (1)$ in $2 π i Z$ , and $F : = G - G (1)$ is holomorphic with $\exp \circ F = h$ and $F (1) = 0$ .

step 2.1L1L12

4.1

Fix $z \in S$ and let $ϕ (t) = Im F (1 + t (z - 1))$ for $t \in [0, 1]$ ; the segment lies in $S$ by step 1.2, and $ϕ$ is continuous by [L13] and [L14], with $ϕ (0) = 0$ . If $∣ ϕ (1) ∣ \geq π$ then [L8] gives $t$ with $ϕ (t) = π$ or $ϕ (t) = - π$ ; writing $w = 1 + t (z - 1)$ and using $\exp (F (w)) = w$ together with [L7], [L11] and [L14] gives $w = e^{Re F (w)} (\cos (\pm π) + i \sin (\pm π)) = - e^{Re F (w)}$ , a real number $< 0$ , contradicting $w \in S$ . Hence $Im F (z) \in (- π, π)$ .

step 1.2step 3.1L7L8L11L13L14

5.1

By [L6] there is an integer $k$ with $F (z) = Log z + 2 π i k$ ; taking imaginary parts and using [L4] and [L5], $Im F (z) = θ + 2 π k$ with $- π < θ \leq π$ , and step 4.1 gives $Im F (z) \in (- π, π)$ , so $2 π k \in (- 2 π, 2 π)$ and therefore $k = 0$ by [L16]. Hence $F = Log$ on $S$ .

step 3.1step 4.1L4L5L6L14L16

6.1

By step 5.1 the principal logarithm is holomorphic on $S$ , and [L3] applied to $L = Log$ and $h (z) = z$ gives ${Log}^{'} (z) = 1 / z$ there. If $F_{1}$ is any holomorphic function on $S$ with $\exp \circ F_{1} = h$ and $F_{1} (1) = 0$ , then $F_{1} - Log$ is a constant in $2 π i Z$ by [L1], and it vanishes at $1$ , so $F_{1} = Log$ .

step 5.1L1L3∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

83 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

J. Lebl, Complex Analysis, Ch. 4 §4.3 (standard reference, not scraped)