Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 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 homologically simply connected domain has a holomorphic logarithm

Statement

Let Ω be a homologically simply connected complex domain and let f:Ω→C be holomorphic and nowhere zero. Then there is a holomorphic L:Ω→C with

exp⁡(L(z))=f(z)(z∈Ω),

and any two such functions differ by a constant lying in 2πiZ.

Facts & Assumptions

Given: A homologically simply connected complex domain Ω and a holomorphic nowhere-zero f:Ω→C.

[L1]

Every holomorphic function on a homologically simply connected complex domain has a primitive there (Every holomorphic function on a homologically simply connected domain has a primitive), that is a holomorphic F with F′ equal to the function (A primitive of a complex function on an open set).

[L2]

The complex exponential maps C onto C∖{0} (The complex exponential maps C onto C∖{0}).

[L3]

The complex exponential is entire with exp⁡′=exp⁡ (The complex exponential is entire and its complex derivative is itself).

[L4]

If f is complex differentiable at a and g at f(a), then (g∘f)′(a)=g′(f(a))f′(a) (The chain rule for complex derivatives).

[L5]

Linear combinations, products and nonvanishing quotients of functions complex differentiable at a point are complex differentiable there, with the usual formulas (Linearity, product, reciprocal, and quotient rules for complex derivatives).

[L6]

If U is a complex domain and g:U→C is holomorphic with g′≡0, then g is constant on U (A holomorphic function with zero derivative on a domain is constant).

[L7]

ker⁡(exp⁡)=2πiZ, and exp⁡z=exp⁡w exactly when z−w∈2πiZ (ker⁡(exp⁡)=2πiZ, and exp⁡z=exp⁡w exactly when z−w∈2πiZ).

[L8]

Every holomorphic function has complex derivatives of all natural orders locally (All higher complex derivatives exist and satisfy Cauchy's integral formula on an interior circle); a complex differentiable function is continuous (Complex differentiability at a point implies continuity there).

[L10]

A complex domain is a nonempty, connected, open subset of C (A complex domain is a nonempty connected open subset of C), and a homologically simply connected domain is such a domain in which every cycle is null-homologous (Homologically simply connected complex domains).

[L11]

For z=a+bi with a,b real, Im⁡z=b and ∣z∣=a2+b2 (Real and imaginary parts, complex conjugation, and modulus); the integers form an ordered commutative ring and are discrete in R, so if m<n then m+12 lies strictly between them and is not an integer (The integers form a commutative ring, The integers form a totally ordered ring, Integer part: for every real x there is exactly one integer m with m≤x<m+1).

[L13]

exp⁡(z+w)=exp⁡z exp⁡w for all complex z,w, hence exp⁡(−w)exp⁡(w)=1 (exp⁡(z+w)=exp⁡z exp⁡w, and the complex exponential extends the real exponential).

Proof

technique · direct
1.1givenL5L8

By [L8] the derivative f′ is holomorphic on Ω, and f is nowhere zero, so the logarithmic derivative f′/f is holomorphic on Ω by [L5].

1.2givenL2L10

Fix z0∈Ω, which is nonempty by [L10]. Since f(z0)≠0, [L2] gives w0∈C with exp⁡(w0)=f(z0).

2.1step 1.1step 1.2L1L5

By [L1] the function f′/f of step 1.1 has a primitive G on Ω; put F=G−G(z0)+w0, so that F is holomorphic with F′=f′/f and F(z0)=w0.

3.1step 2.1L3L4L5L6L10

The function u=fexp⁡(−F) is holomorphic on Ω by [L3], [L4] and [L5], and u′=f′exp⁡(−F)−fF′exp⁡(−F)=(f′−f⋅(f′/f))exp⁡(−F)=0 throughout Ω; so u is a constant by [L6] and [L10].

4.1step 1.2step 2.1step 3.1L13

Evaluating at z0 gives that constant: u(z0)=f(z0)exp⁡(−w0)=exp⁡(w0)exp⁡(−w0)=1 by step 1.2 and [L13], so f=exp⁡(F) on Ω and L=F has the required property.

5.1step 4.1L7L8L9L10L11L12∎

If L1,L2 are holomorphic on Ω with exp⁡∘L1=exp⁡∘L2=f, then L1−L2 takes values in 2πiZ by [L7]; it is continuous by [L8], so Im⁡(L1−L2)/(2π) is a continuous integer-valued real function by [L11] and [L12], and [L9] with [L10] and [L11] forces it to be constant on the connected Ω. Hence L1−L2 is a constant in 2πiZ.

Depends on

Used by

Dependency tree · two levels

111 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