TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-02

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.

There is no continuous logarithm on all of $C ∖ {0}$

Statement

There is no continuous function $L : C ∖ {0} \to C$ satisfying $\exp (L (z)) = z$ for every $z \neq 0$ . The conventions and prerequisite facts used below are recorded in Complex logarithms, the principal logarithm, and principal and multivalued complex powers, $\ker (\exp) = 2 π i Z$ , and $\exp z = \exp w$ exactly when $z - w \in 2 π i Z$ , $\exp (z + w) = \exp z \exp w$ , and the complex exponential extends the real exponential, The Euclidean metric, convergence, Cauchy sequences, and continuity on the complex plane, Euler's formula: $\exp (i θ) = \cos θ + i \sin θ$ for every real $θ$ , The derivatives of sine and cosine are cosine and minus sine, A vector-valued function has a limit, or is continuous, if and only if each of its components does; with the algebra of continuous vector-valued functions, and 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)$ .

Facts & Assumptions

Given: The unit-circle path $γ (t) = \exp (i t)$ for $0 \leq t \leq 2 π$ .

[L1]

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

[L2]

Euler's formula: $\exp (i θ) = \cos θ + i \sin θ$ for every real $θ$ gives $γ (t) = \cos t + i \sin t$ , and The derivatives of sine and cosine are cosine and minus sine makes both real coordinate functions continuous.

[L3]

A vector-valued function has a limit, or is continuous, if and only if each of its components does; with the algebra of continuous vector-valued functions makes a complex-valued map continuous exactly when its two real components are continuous.

[L4]

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)$ gives every intermediate real value of a continuous real function on a closed interval.

[L5]

The Euclidean metric, convergence, Cauchy sequences, and continuity on the complex plane defines continuity on subsets of $C$ by its Euclidean metric.

Proof

technique · contradiction

1.1

Suppose such a continuous $L$ exists and put $h (t) = L (γ (t)) - i t$ . By [L2], [L3], and [L5], $γ$ , $L \circ γ$ , and $h$ are continuous on $[0, 2 π]$ .

assume-contraL2L3L5

2.1

The assumed identity says $\exp (L (γ (t))) = γ (t) = \exp (i t)$ . Hence [L1] gives $h (t) \in 2 π i Z$ for every $t$ .

L1step 1.1

3.1

By [L3], $ν (t) : = Im (h (t)) / (2 π)$ is a continuous real-valued function; by step 2.1 it takes values in $Z$ . If $ν (s) \neq ν (t)$ for some $s < t$ , [L4] applied to $ν$ on $[s, t]$ gives a noninteger value strictly between two distinct integers, a contradiction. Thus $ν$ is constant.

L3L4step 2.1

4.1

Euler's formula gives $γ (0) = γ (2 π) = 1$ , so $h (2 π) = L (1) - 2 π i = h (0) - 2 π i$ . Its imaginary quotient therefore changes by $- 1$ , contradicting step 3.1.

L2step 1.1step 3.1discharge-contradiction∎

Depends on

Used by

A nonvanishing holomorphic function on a domain with no holomorphic logarithm Counterexample
log|z| has no global harmonic conjugate on C{0 Counterexample

Dependency tree · two levels

70 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, Basic Analysis I: Complex Numbers and the Complex Exponential (standard reference, not scraped)

There is no continuous logarithm on all of C∖{0}C∖{0}