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 , the identity function on it, and the contour on .
On a homologically simply connected complex domain, a holomorphic nowhere-zero function admits a holomorphic with 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).
There is no continuous with for every (There is no continuous logarithm on all of ).
If and are holomorphic on an open set with , then is nowhere zero and (A holomorphic logarithm is a primitive of the logarithmic derivative).
For a positively oriented circle with , (The normalized integral around a positively oriented circle centred at a is 1).
If is holomorphic on an open set, is continuous there, and is a closed rectifiable contour in that set, then (The integral of a continuous complex derivative over every closed rectifiable contour is zero).
A cycle with trace in an open is null-homologous in when its index vanishes at every point of (Null-homologous cycles and homologous cycles in an open set).
The annulus is a complex domain that is not homologically simply connected, the unit circle in it having index about the origin (A connected plane domain that is not homologically simply connected).
For , and , the contour on is a closed complex contour with index for and for , with trace when (A circle traversed times has winding number inside and outside).
A complex domain is a nonempty, connected, open subset of (A complex domain is a nonempty connected open subset of ); for and the set is path-connected and connected, and at this is the punctured plane (The exterior of a closed disc in the plane is path-connected).
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 (Linearity, product, reciprocal, and quotient rules for complex derivatives).
A single closed contour with coefficient 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).
A set is open exactly when each of its points admits a ball inside it (The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement, Open ball, closed ball and sphere in a metric space).
Counterexample
Take and on it.
is a complex domain: it is nonempty, open by [L12], and connected by [L9] with and . The function is holomorphic on by [L10] and nowhere zero there, since .
Suppose were a holomorphic function on with for every . Then is continuous on by [L10], contradicting [L2]; so no such exists and the claim is refuted.
A second refutation, independent of [L2]. With as in step 3.1, [L3] gives , which is continuous on by [L10], so [L5] applied to the closed rectifiable contour in gives ; but [L4] gives .
The hypothesis of [L1] that fails is homological simple connectivity: by [L8] and [L11] the unit circle is a cycle with trace in and , while , so is not null-homologous in by [L6]. The same failure on the smaller annulus is recorded in [L7].
Depends on
- A nonvanishing holomorphic function on a homologically simply connected domain has a holomorphic logarithm
- There is no continuous logarithm on all of $\mathbb C\setminus\{0\}$
- A holomorphic logarithm is a primitive of the logarithmic derivative
- The normalized integral around a positively oriented circle centred at a is 1
- The integral of a continuous complex derivative over every closed rectifiable contour is zero
- Homologically simply connected complex domains
- Null-homologous cycles and homologous cycles in an open set
- A connected plane domain that is not homologically simply connected
- A circle traversed $k$ times has winding number $k$ inside and $0$ outside
- A complex domain is a nonempty connected open subset of $\mathbb C$
- The exterior of a closed disc in the plane is path-connected
- Complex differentiability at a point implies continuity there
- Linearity, product, reciprocal, and quotient rules for complex derivatives
- Complex chains, their traces, and cycles
- Integration over a complex chain and the index of a chain
- The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement
- Open ball, closed ball and sphere in a metric space
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
- J. Lebl, Complex Analysis, Ch. 4 §4.3 (standard reference, not scraped)