Alphabeta Math
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.

A nonvanishing holomorphic function on a domain with no holomorphic logarithm

Statement refuted

Every holomorphic nowhere-zero function on a complex domain has a holomorphic logarithm on that domain.

Facts & Assumptions

Given: The punctured plane U=C{0}, the identity function f(z)=z on it, and the contour C(t)=exp(it) on [0,2π].

[L1]

On a homologically simply connected complex domain, a holomorphic nowhere-zero function admits a holomorphic L with expL equal to it (A nonvanishing holomorphic function on a homologically simply connected domain has a holomorphic logarithm), a domain being homologically simply connected when every cycle in it is null-homologous in it (Homologically simply connected complex domains).

[L2]

There is no continuous L:C{0}C with exp(L(z))=z for every z0 (There is no continuous logarithm on all of C{0}).

[L3]

If L and h are holomorphic on an open set with expL=h, then h is nowhere zero and L=h/h (A holomorphic logarithm is a primitive of the logarithmic derivative).

[L4]

For a positively oriented circle a+rexp(it) with r>0, (2πi)1γdz/(za)=1 (The normalized integral around a positively oriented circle centred at a is 1).

[L5]

If F is holomorphic on an open set, F is continuous there, and γ is a closed rectifiable contour in that set, then γF(z)dz=0 (The integral of a continuous complex derivative over every closed rectifiable contour is zero).

[L6]

A cycle with trace in an open Ω is null-homologous in Ω when its index vanishes at every point of CΩ (Null-homologous cycles and homologous cycles in an open set).

[L7]

The annulus {12<z<2} is a complex domain that is not homologically simply connected, the unit circle in it having index 1 about the origin (A connected plane domain that is not homologically simply connected).

[L8]

For aC, r>0 and kZ, the contour a+rexp(ikt) on [0,2π] is a closed complex contour with index k for za<r and 0 for za>r, with trace {za=r} when k0 (A circle traversed k times has winding number k inside and 0 outside).

[L9]

A complex domain is a nonempty, connected, open subset of C (A complex domain is a nonempty connected open subset of C); for cC and R0 the set {z:zc>R} is path-connected and connected, and at R=0 this is the punctured plane (The exterior of a closed disc in the plane is path-connected).

[L10]

A complex differentiable function is continuous (Complex differentiability at a point implies continuity there), and linear combinations, products and nonvanishing quotients of complex differentiable functions are complex differentiable, the identity having derivative 1 (Linearity, product, reciprocal, and quotient rules for complex derivatives).

[L11]

A single closed contour with coefficient 1 is a cycle whose trace is that contour's trace (Complex chains, their traces, and cycles) and whose index is that contour's winding number (Integration over a complex chain and the index of a chain).

Counterexample

technique · constructive
1.1

Take U=C{0} and f(z)=z on it.

givenconstruct
2.1

U is a complex domain: it is nonempty, open by [L12], and connected by [L9] with c=0 and R=0. The function f is holomorphic on U by [L10] and nowhere zero there, since 0U.

step 1.1L9L10L12
3.1

Suppose L were a holomorphic function on U with exp(L(z))=z for every zU. Then L is continuous on U by [L10], contradicting [L2]; so no such L exists and the claim is refuted.

step 2.1L2L10
4.1

A second refutation, independent of [L2]. With L as in step 3.1, [L3] gives L(z)=1/z, which is continuous on U by [L10], so [L5] applied to the closed rectifiable contour C in U gives Cdz/z=CL(z)dz=0; but [L4] gives Cdz/z=2πi0.

step 2.1L3L4L5L10
5.1

The hypothesis of [L1] that fails is homological simple connectivity: by [L8] and [L11] the unit circle C is a cycle with trace in U and n(C,0)=1, while 0CU, so C is not null-homologous in U by [L6]. The same failure on the smaller annulus is recorded in [L7].

step 3.1step 4.1L1L6L7L8L11discharge-construct

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

86 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