Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

Holomorphic inverse function theorem and local-degree criterion

Statement

For a nonconstant holomorphic map, nonzero derivative, local degree one, local injectivity, and local biholomorphy are equivalent.

Precisely, let f be nonconstant and holomorphic on a complex domain Ω, and let aΩ. The following are equivalent:

  1. f(a)0;
  2. degaf=1 (Local degree of a nonconstant holomorphic map);
  3. f is locally injective at a (Locally injective holomorphic maps);
  4. f is biholomorphic between neighbourhoods of a and f(a) (Biholomorphic maps between complex domains).

For a local inverse g, one has g(w)=1f(g(w)) throughout its domain.

Facts & Assumptions

Given: A nonconstant holomorphic function f on a complex domain Ω and a point aΩ. The complex chain rule applies to inverse identities (The chain rule for complex derivatives).

[L1]

If f is holomorphic near a and f(a)0, then f is biholomorphic between neighbourhoods of a and f(a) (A nonzero complex derivative gives a local biholomorphism).

[L2]

For every neighbourhood N of a, there are a smaller open neighbourhood VN and a real ρ>0 such that every w with 0<wf(a)<ρm, where m=degaf, has exactly m distinct preimages in V (A local degree-m holomorphic map has m nearby sheets).

[L3]

A holomorphic function has finite order m at a exactly when, on some neighbourhood of a, it is (za)mq(z) with q holomorphic and q(a)0 (The order of a zero is the exponent in its local holomorphic factorization).

Proof

technique · direct
1.1

For the equivalence between claims 1 and 2, [L3] gives f(z)f(a)=(za)mq(z) with m=degaf and q(a)0. If m=1, differentiation at a gives f(a)=q(a)0; if m>1, it gives f(a)=0. Thus f(a)0 exactly when degaf=1.

L3givenalgebra
1.2

For the implication from claim 1 to claim 4, [L1] directly makes f biholomorphic between neighbourhoods of a and f(a).

L1assume-hyp
1.3

For the implication from claim 4 to claim 3, a biholomorphic restriction is bijective and hence injective on its source neighbourhood.

assume-hyp
2.1

For the converse implication from claim 3 back to claim 2, suppose f is injective on a neighbourhood N of a. If m=degaf>1, take VN and ρ>0 from [L2] and put w:=f(a)+ρm/2. Then w has m>1 distinct preimages in V, contradicting injectivity on N. Since m is positive, m=1, and step 1.1 then gives f(a)0.

L2step 1.1assume-hypchoose
3.1

For the derivative formula, let g be the inverse supplied in step 1.2. Differentiating g(f(z))=z gives g(f(z))f(z)=1, so, writing w=f(z), one obtains g(w)=1/f(g(w)).

step 1.2givenalgebra

Depends on

Used by

Dependency tree · two levels

28 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