CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-17

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 holomorphic function on an annulus can have a nonzero closed-contour integral

Statement refuted

Refuted claim: If $U$ is a complex domain, $f$ is holomorphic on $U$ , and $γ$ is a closed rectifiable contour in $U$ , then $\int_{γ} f (z) d z = 0$ .

Take

$A = {z \in C : \frac{1}{2} < ∣ z ∣ < 2}, f (z) = \frac{1}{z},$

and let $γ (t) = \exp (i t)$ , $0 \leq t \leq 2 π$ , be the positively oriented unit circle. Then $A$ is a complex domain, $f$ is holomorphic on $A$ , and

$\int_{γ} f (z) d z = 2 π i \neq 0.$

Facts & Assumptions

Given: The annulus $A$ , the function $f (z) = 1 / z$ , and the unit circle $γ$ .

[L1]

The modulus is multiplicative and satisfies the triangle inequality, hence $∣ ∣ z ∣ - ∣ w ∣ ∣ \leq ∣ z - w ∣$ (Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive).

[L2]

A rational function is holomorphic wherever its denominator is nonzero (Complex polynomials are entire with the power-rule derivative, and rational functions are holomorphic wherever their denominator is nonzero).

[L3]

Every nonzero complex number has a polar representation $r (\cos θ + i \sin θ)$ with $r > 0$ , and $\exp (i θ) = \cos θ + i \sin θ$ for real $θ$ (Every nonzero complex number has a unique polar form $r (\cos θ + i \sin θ)$ with $r > 0$ and $- π < θ \leq π$ , $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ ).

[L4]

A space is path-connected when each pair of points is joined by a continuous path, and every path-connected space is connected (Paths, path-connected spaces and path components, Every path-connected space is connected, and every path component lies inside a component).

[L5]

A complex domain is a nonempty connected open subset of $C$ (A complex domain is a nonempty connected open subset of $C$ ).

[L6]

The integral of $z^{- 1}$ around the positively oriented unit circle is $2 π i$ (On a positively oriented circle about a, the integral of (z-a)^m is zero for every integer m except -1, and is 2 pi i for m=-1).

[L7]

The complex exponential is entire and therefore continuous (The complex exponential is entire and its complex derivative is itself, Complex differentiability at a point implies continuity there).

Refutation

technique · direct

1.1

The point $1$ lies in $A$ . For $z \in A$ , let $δ = \frac{1}{2} \min {∣ z ∣ - 1 / 2, 2 - ∣ z ∣} > 0$ ; if $∣ w - z ∣ < δ$ , [L1] gives $1 / 2 < ∣ w ∣ < 2$ , so $A$ is open.

givenL1

1.2

Given $z = r \exp (i θ)$ and $w = s \exp (i ϕ)$ in $A$ as in [L3], the radial paths $t \mapsto ((1 - t) r + t) \exp (i θ)$ and $t \mapsto ((1 - t) s + t) \exp (i ϕ)$ stay in $A$ , and the unit-circle arc $t \mapsto \exp (i ((1 - t) θ + t ϕ))$ joins their unit endpoints. By [L7] these paths are continuous; the first, the arc, and the reversal of the second concatenate to join $z$ to $w$ , so [L4] makes $A$ path-connected and connected.

L3L4L7

2.1

Steps 1.1 and 1.2 show that $A$ is nonempty, open, and connected, hence a complex domain by [L5]; since $0 \notin A$ , [L2] makes $f (z) = 1 / z$ holomorphic on $A$ .

step 1.1step 1.2L2L5

3.1

The unit circle is a closed rectifiable contour in $A$ , while [L6] gives its integral as $2 π i \neq 0$ . Thus the displayed domain, function, and contour refute the claim.

step 2.1L6∎

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: 188 results over 25 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

Richard Howell and John Mathews, Complex Analysis, Example 6.4.9 (standard reference, not scraped)