CounterexampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 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.

A biholomorphism between the disc and the punctured disc cannot exist

Statement refuted

There is a biholomorphism from $D$ onto $D ∖ {0}$ .

Facts & Assumptions

Given: The claimed biholomorphism $f : D \to D ∖ {0}$ and its holomorphic inverse $g : D ∖ {0} \to D$ .

[L1]

A bounded holomorphic function on a punctured disc has a removable singularity at the puncture exactly when it extends holomorphically there (Characterizations of removable singularities).

[L2]

A nonconstant holomorphic map is open (Open mapping theorem for holomorphic functions).

Counterexample

technique · direct

1.1

The inverse $g$ is bounded by $1$ on $D ∖ {0}$ , so [L1] extends it across the puncture to a holomorphic map $G : D \to C$ . Continuity gives $∣ G ∣ \leq 1$ on the full disc.

L1given

2.1

The map $G$ is nonconstant because it agrees with the inverse $g$ off the puncture. If $∣ G (0) ∣ = 1$ , [L2] would make $G (D)$ an open set containing a boundary point of the closed unit disc, contradicting $∣ G ∣ \leq 1$ . Hence $G (0) \in D$ .

L2step 1.1assume-contradischarge-contradiction

3.1

For every nonzero $z \in D$ , the inverse identity gives $f (G (z)) = f (g (z)) = z$ . Letting $z \to 0$ and using step 2.1 plus continuity of $f$ gives $f (G (0)) = 0$ . This contradicts $f (D) = D ∖ {0}$ , so no such biholomorphism exists.

step 1.1step 2.1algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

13 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

Walter Rudin, Real and Complex Analysis, Ch. 14 (standard reference, not scraped)