TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24

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.

Local normal form of a nonconstant holomorphic map

Statement

Let $f : Ω \to C$ be nonconstant and holomorphic on a complex domain $Ω$ , let $a \in Ω$ , and put $m = \deg_{a} f$ . Then near $a$ there is a biholomorphic coordinate $ϕ$ with $ϕ (a) = 0$ and $f (z) - f (a) = ϕ (z)^{m}$ .

Precisely, there is a complex domain $V$ with $a \in V \subseteq Ω$ such that $ϕ : V \to ϕ [V]$ is biholomorphic, $ϕ (a) = 0$ , and the displayed identity holds for every $z \in V$ .

Facts & Assumptions

Given: A nonconstant holomorphic function $f$ on a complex domain $Ω$ , a point $a \in Ω$ , and the positive natural $m = \deg_{a} f$ (Local degree of a nonconstant holomorphic map). Holomorphic products obey the product rule (Linearity, product, reciprocal, and quotient rules for complex derivatives).

[L1]

A holomorphic function has finite order $m$ at $a$ exactly when, near $a$ , it has the form $(z - a)^{m} h (z)$ with $h$ holomorphic and $h (a) \neq 0$ (The order of a zero is the exponent in its local holomorphic factorization).

[L2]

For every positive natural $m$ , a nowhere-zero holomorphic function on a disc has a holomorphic $m$ th root (Holomorphic roots of a nonvanishing function on a disc).

[L3]

If a function is holomorphic near $a$ and has nonzero derivative at $a$ , then it is biholomorphic between neighbourhoods of $a$ and its value (A nonzero complex derivative gives a local biholomorphism).

[L4]

A complex differentiable function is continuous at every point of complex differentiability (Complex differentiability at a point implies continuity there).

Proof

technique · direct

1.1L1given

Apply [L1] to $f - f (a)$ : on a neighbourhood of $a$ one has $f (z) - f (a) = (z - a)^{m} h (z)$ , where $h$ is holomorphic and $h (a) \neq 0$ .

2.1step 1.1L2L4

Since $h (a) \neq 0$ , [L4] permits shrinking to a disc on which $h$ is nowhere zero. By [L2] there is a holomorphic $q$ on that disc with $q^{m} = h$ .

3.1step 2.1L3givenalgebra

Define $ϕ (z) : = (z - a) q (z)$ . Then $ϕ (a) = 0$ and the product rule gives $ϕ^{'} (a) = q (a) \neq 0$ , so [L3] makes $ϕ$ biholomorphic after one further shrinking around $a$ .

4.1step 1.1step 2.1step 3.1algebra∎

On that final neighbourhood, steps 1.1 and 2.1 give $f (z) - f (a) = (z - a)^{m} q (z)^{m} = ϕ (z)^{m}$ , which is the required normal form.

Depends on

Used by

Dependency tree · two levels

29 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, Guide to Cultivating Complex Analysis, Theorem 5.1.3 (standard reference, not scraped)