CorollaryStatement: 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 holomorphic logarithm is a primitive of the logarithmic derivative

Statement

Let $U \subseteq C$ be open and let $L, h : U \to C$ be holomorphic with $\exp (L (z)) = h (z)$ for every $z \in U$ . Then $h$ is nowhere zero on $U$ and

$L^{'} (z) = \frac{h^{'} (z)}{h (z)} (z \in U) .$

In particular, if $p \in C$ , if $U$ misses $p$ , and if $L$ is holomorphic on $U$ with $\exp (L (z)) = z - p$ for every $z \in U$ , then $L^{'} (z) = 1 / (z - p)$ on $U$ .

Facts & Assumptions

Given: An open $U \subseteq C$ and holomorphic $L, h : U \to C$ with $\exp \circ L = h$ .

[L1]

The complex exponential is entire and $\exp^{'} (z) = \exp z$ for every $z \in C$ (The complex exponential is entire and its complex derivative is itself).

[L2]

If $f : U \to V$ is complex differentiable at $a$ and $g : V \to C$ is complex differentiable at $f (a)$ , then $(g \circ f)^{'} (a) = g^{'} (f (a)) f^{'} (a)$ (The chain rule for complex derivatives).

[L3]

Linear combinations and products of functions complex differentiable at a point are complex differentiable there, with the usual formulas; if $g (a) \neq 0$ then $(f / g)^{'} (a) = (f^{'} (a) g (a) - f (a) g^{'} (a)) / g (a)^{2}$ ; every constant function has derivative $0$ and the identity function has derivative $1$ (Linearity, product, reciprocal, and quotient rules for complex derivatives).

[L4]

For real $x, y$ , $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ and $∣ \exp (x + i y) ∣ = e^{x}$ ( $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ ).

[L5]

A function is holomorphic on an open $U$ when it is complex differentiable at every point of $U$ (Complex differentiability at a point, the complex derivative, holomorphic functions, and entire functions).

Proof

technique · direct

1.1givenL4

For every $v \in C$ , writing $v = x + i y$ with $x, y$ real, [L4] gives $∣ \exp v ∣ = e^{x} > 0$ , so $\exp$ never vanishes; hence $h = \exp \circ L$ is nowhere zero on $U$ .

1.2givenL1L2L5

By [L5] both $L$ and $h$ are complex differentiable at every point of $U$ , and [L1] and [L2] give $(\exp \circ L)^{'} (z) = \exp (L (z)) L^{'} (z)$ there.

2.1givenstep 1.1step 1.2algebra

Since $\exp \circ L = h$ as functions on $U$ , step 1.2 says $h^{'} (z) = h (z) L^{'} (z)$ for every $z \in U$ ; dividing by the nonzero $h (z)$ of step 1.1 gives $L^{'} (z) = h^{'} (z) / h (z)$ .

3.1step 2.1L3∎

If $U$ misses $p$ and $h (z) = z - p$ on $U$ , then $h^{'} (z) = 1$ by [L3], so step 2.1 gives $L^{'} (z) = 1 / (z - p)$ on $U$ .

Depends on

Used by

Dependency tree · two levels

23 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

L. V. Ahlfors, Complex Analysis, 3rd ed., Ch. 4 §2.1 (standard reference, not scraped)
J. Lebl, Complex Analysis, Ch. 4 §4.1 (standard reference, not scraped)