CounterexampleConstruction: Literature-sourcedVerification: 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.

e^{1/z} has an essential singularity at 0 and omits the value 0

Statement refuted

Refuted claim: an essential singularity attains every complex value on each punctured neighbourhood.

The witness is

$f (z) = e^{1 / z}$

at $a = 0$ . The singularity is essential, but the value $0$ is omitted on every punctured neighbourhood of $0$ .

Facts & Assumptions

Given: The function $f (z) = e^{1 / z}$ on $0 < ∣ z ∣ < 1$ .

[L1]

Every isolated singularity is removable, a pole, or essential (Every isolated singularity is removable, a pole, or essential).

[L2]

The complex exponential is entire (The complex exponential is entire and its complex derivative is itself).

[L3]

The exponential satisfies $\exp (u + v) = \exp (u) \exp (v)$ for all complex $u, v$ ( $\exp (z + w) = \exp z \exp w$ , and the complex exponential extends the real exponential).

Counterexample

technique · direct

1.1

Since $z \mapsto 1 / z$ is holomorphic on $0 < ∣ z ∣ < 1$ and $\exp$ is entire by [L2], the function $f (z) = e^{1 / z}$ is holomorphic on $0 < ∣ z ∣ < 1$ .

L2algebra

1.2

If $e^{1 / z_{0}} = 0$ for some $z_{0} \neq 0$ , then [L3] gives $1 = e^{1 / z_{0}} e^{- 1 / z_{0}} = e^{0} = 0$ , impossible. Hence $e^{1 / z}$ never takes the value $0$ .

L3algebra

2.1

Along the positive real axis, $f (t) = e^{1 / t} \to \infty$ as $t ↓ 0$ , so the singularity is not removable. Along the negative real axis, $f (- t) = e^{- 1 / t} \to 0$ as $t ↓ 0$ , so the singularity is not a pole.

step 1.1algebra

3.1

By [L1], a singularity that is neither removable nor a pole is essential, so $0$ is an essential singularity of $e^{1 / z}$ .

step 2.1L1

4.1

Thus $e^{1 / z}$ has an essential singularity at $0$ and still omits the value $0$ , refuting the claim and showing why Casorati-Weierstrass theorem gives density rather than surjectivity.

step 3.1step 1.2∎

Depends on

Used by

A Laurent series on a punctured disc can have infinitely many negative powers Counterexample

Dependency tree · two levels

22 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

David Greenfield, Rutgers Math 403 diary (standard reference, not scraped)