TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-08-29

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.

Branch-defined complex powers agree with integer powers

Statement

Let $V \subseteq C$ be open with $0 \notin V$ and let $L : V \to C$ be a holomorphic logarithm branch of $z$ on $V$ . For every integer $n \in Z$ and every $z \in V$ , the branch power of Complex powers defined from a holomorphic logarithm branch equals the complex integer power of Integer powers in the complex field:

$z_{L}^{n} : = \exp (n L (z)) = z^{n} .$

In particular $\exp (n L (z))$ is independent of the choice of branch $L$ : the right-hand side $z^{n}$ mentions no logarithm at all.

Facts & Assumptions

Given: An open $V \subseteq C$ with $0 \notin V$ , a holomorphic logarithm branch $L$ of $z$ on $V$ , an integer $n$ , and $z \in V$ .

[F1]

A holomorphic logarithm branch $L$ of $z$ on $V$ satisfies $\exp (L (z)) = z$ for every $z \in V$ , and its branch power is $z_{L}^{α} : = \exp (α L (z))$ (Complex powers defined from a holomorphic logarithm branch).

[F2]

The complex integer powers satisfy $z^{0} = 1$ , $z^{m + 1} = z^{m} z$ for $m \in N$ , and $z^{r} : = (z^{m})^{- 1}$ when $r < 0$ with $- r$ the natural $m \geq 1$ (Integer powers in the complex field).

[F3]

For all $u, v \in C$ , $\exp (u + v) = \exp u \exp v$ ; for real $x$ , the complex value $\exp (x + 0 i)$ equals the real exponential $e^{x}$ ( $\exp (z + w) = \exp z \exp w$ , and the complex exponential extends the real exponential).

[F4]

The complex exponential is $\exp z = \sum_{n \geq 0} z^{n} / n!$ for every $z \in C$ , so $\exp 0 = 1$ (The complex exponential by its power series).

Proof

technique · induction on the nonnegative integer $m$ with $\exp(mL(z))=z^m$

1.1F1F2F4base

Base case: $z_{L}^{0} = \exp (0 \cdot L (z)) = \exp 0 = 1 = z^{0}$

1.2ihassume-hyp

Assume for a fixed $m \geq 0$ that $\exp (m L (z)) = z^{m}$ .

2.1F1F2F3step 1.2ih

By [F3] and [F1], $\exp ((m + 1) L (z)) = \exp (m L (z)) \exp (L (z)) = z^{m} z = z^{m + 1}$

3.1F2F3F4step 2.1

For $r = - m < 0$ : [F3] and [F4] give $\exp (- m L (z)) \exp (m L (z)) = \exp 0 = 1$ , so by step 2.1 and [F2], $\exp (- m L (z)) = (z^{m})^{- 1} = z^{- m} = z^{r}$ .

4.1step 2.1step 3.1discharge-induction∎

Steps 2.1 and 3.1 cover every integer, so $z_{L}^{n} = z^{n}$ ; the right side mentions no branch, giving independence.

Depends on

Used by

Dependency tree · two levels

19 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

Lars V. Ahlfors, Complex Analysis, 3rd ed., Ch. 2 (standard reference, not scraped)