Alphabeta Math
CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck 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 ∫γf(z) dz=0.

Take

A={z∈C:12<∣z∣<2},f(z)=1z,

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

∫γf(z) dz=2πi≠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∣∣≤∣z−w∣ (Conjugation is an involutive real-field automorphism, zz‾=∣z∣2, and modulus is definite, multiplicative, and subadditive).

[L3]

Every nonzero complex number has a polar representation r(cos⁡θ+isin⁡θ) with r>0, and exp⁡(iθ)=cos⁡θ+isin⁡θ for real θ (Every nonzero complex number has a unique polar form r(cos⁡θ+isin⁡θ) with r>0 and −π<θ≤π, exp⁡(x+iy)=ex(cos⁡y+isin⁡y), ∣exp⁡(x+iy)∣=ex, and eiπ+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).

Refutation

technique · direct
1.1givenL1

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

1.2L3L4L7

Given z=rexp⁡(iθ) and w=sexp⁡(iϕ) in A as in [L3], the radial paths t↦((1−t)r+t)exp⁡(iθ) and t↦((1−t)s+t)exp⁡(iϕ) stay in A, and the unit-circle arc t↦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.

2.1step 1.1step 1.2L2L5

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

3.1step 2.1L6∎

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

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

53 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