ExampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passaudited 2026-08-30

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 function e^(1/z) omits zero and takes every nonzero value infinitely often near the origin

Example

The function

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

on $0 < ∣ z ∣ < 1$ omits $0$ and takes every nonzero value infinitely often near $0$ .

Facts & Assumptions

Given: The punctured-disc function $f (z) = e^{1 / z}$ .

[L1]

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

[L2]

Its fibres are the translates $\log w + 2 π i k$ ( $\ker (\exp) = 2 π i Z$ , and $\exp z = \exp w$ exactly when $z - w \in 2 π i Z$ ).

Verification

technique · direct

1.1

Since the exponential never vanishes, $f (z)$ never equals $0$ on the punctured disc.

L1given

1.2

Fix $w \neq 0$ . By [L1] and [L2], choose $λ \in C$ with $e^{λ} = w$ ; then every number $λ + 2 π i k$ is another logarithm of $w$ . For every integer $k$ with $λ + 2 π i k \neq 0$ , set $z_{k} : = 1 / (λ + 2 π i k)$ . At most one integer is excluded, while all the remaining $z_{k}$ satisfy $f (z_{k}) = w$ and $z_{k} \to 0$ as $∣ k ∣ \to \infty$ . Thus every nonzero value occurs infinitely often near $0$ .

L1L2givenconstruct

2.1

Therefore Great Picard is sharp: one finite exceptional value can occur, namely $0$ .

step 1.1step 1.2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

16 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

Aleksander Simonic, The Ahlfors lemma and Picard's theorems, §6.4 (standard reference, not scraped)