TheoremStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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 $\mathbb C\setminus\{0\}$

Statement

There is no continuous function $L:\mathbb C\setminus\{0\}\to\mathbb C$ satisfying $\exp(L(z))=z$ for every $z\ne0$ . The conventions and prerequisite facts used below are recorded in Complex logarithms, the principal logarithm, and principal and multivalued complex powers, $\ker(\exp)=2\pi i\mathbb Z$ , and $\exp z=\exp w$ exactly when $z-w\in2\pi i\mathbb 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\theta)=\cos\theta+i\sin\theta$ for every real $\theta$ , 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 $\gamma(t)=\exp(it)$ for $0\le t\le2\pi$ .

[L1]

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

[L2]

Euler's formula: $\exp(i\theta)=\cos\theta+i\sin\theta$ for every real $\theta$ gives $\gamma(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 $\mathbb C$ by its Euclidean metric.

Proof

technique · contradiction

1.1

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

assume-contraL2L3L5

2.1

The assumed identity says $\exp(L(\gamma(t)))=\gamma(t)=\exp(it)$ . Hence [L1] gives $h(t)\in2\pi i\mathbb Z$ for every $t$ .

L1step 1.1

3.1

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

L3L4step 2.1

4.1

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

L2step 1.1step 3.1discharge-contradiction∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 216 results over 30 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click 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}\mathbb C\setminus\{0\}C∖{0}