Alphabeta Math
Pipeline-generated
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.

✓ 17 results · all verified · 3 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 14 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Conformal Mapping, Branches, and the Schwarz Lemma

1 · Prerequisites

2 · Summary

This page fixes the branch-sensitive conventions that later conformal arguments depend on. It distinguishes the holomorphic principal logarithm on the slit plane from the pointwise principal value on the negative axis, defines branch-based complex powers only after a holomorphic logarithm has been chosen, and records exactly where branch discrepancies obstruct naive product and power laws.

From there the page moves through the disc and upper half-plane models of conformal geometry. Blaschke factors, Schwarz and Schwarz-Pick rigidity, automorphism classifications, and the normalized Poincare metric are assembled before the elementary branch-driven maps: sectors, slit planes, the Joukowski map, and the sine half-strip map. The closing theorem keeps the three simply connected plane models distinct by ruling out biholomorphisms among C^, C, and D.

3 · Logical flowchart

4 · Definitions, theorems and proofs

RemarkRemark: AI-adaptedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-29Open item page →

Dictionary for holomorphic logarithm branches, the principal logarithm, and principal powers

Remark

This page keeps two objects distinct and never silently identifies them.

First, the pointwise principal logarithm of Complex logarithms, the principal logarithm, and principal and multivalued complex powers is defined for every z≠0 by

Log⁡z=log⁡r+iθ,z=r(cos⁡θ+isin⁡θ),−π<θ≤π.

On the negative real axis the principal polar form uses θ=π, so Log⁡(−1)=iπ. That value is a boundary datum of the slit plane, not the value of a holomorphic branch defined across the cut.

Second, Continuous logarithms and continuous arguments along a contour defines a holomorphic logarithm branch of z on an open set V with 0∉V: a holomorphic L:V→C with exp⁡(L(z))=z for every z∈V. On the slit plane S=C∖{x∈R:x≤0} the principal logarithm is exactly the holomorphic branch normalised by F(1)=0, by The principal logarithm is the normalised holomorphic branch on the slit plane; in particular −π<Im⁡Log⁡z<π for every z∈S.

Consequently "the principal branch of the logarithm" on this page means the holomorphic function on S, while the pointwise principal value on the negative axis is a separate quantity: as z approaches −1 from above or below, Im⁡Log⁡z tends to π or −π, one-sided limits that assign no value on the cut itself. The branch-defined powers below take a holomorphic branch as input and inherit this discipline.

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-29Open item page →

Complex powers defined from a holomorphic logarithm branch

Definition

Let V⊆C be open with 0∉V, and let L:V→C be a holomorphic logarithm branch of z on V: L is holomorphic and exp⁡(L(z))=z for every z∈V, the branch vocabulary being that of the dictionary in Dictionary for holomorphic logarithm branches, the principal logarithm, and principal powers. For α∈C define the branch power

zLα:=exp⁡(αL(z))(z∈V).

The subscript records the branch: the same base z can carry many holomorphic logarithm branches, and different branches give different values in general. The defining expression is well formed because the complex exponential is a total function on C, whose values and addition law are those of exp⁡(z+w)=exp⁡z exp⁡w, and the complex exponential extends the real exponential.

The principal branch power is the special case on the slit plane S=C∖{x∈R:x≤0}:

zLog⁡α:=exp⁡(αLog⁡z)(z∈S),

where Log⁡ is the holomorphic principal branch of the dictionary remark. On S this agrees with the pointwise principal power of the published principal-logarithm definition; on the negative axis the pointwise principal value is still defined while the holomorphic branch power is not, and the two are not silently identified.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-29Open item page →

Branch-defined complex powers agree with integer powers

Statement

Let V⊆C be open with 0∉V and let L:V→C be a holomorphic logarithm branch of z on V. For every integer n∈Z and every z∈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:

zLn:=exp⁡(nL(z))=zn.

In particular exp⁡(nL(z)) is independent of the choice of branch L: the right-hand side zn mentions no logarithm at all.

Facts & Assumptions

Given: An open V⊆C with 0∉V, a holomorphic logarithm branch L of z on V, an integer n, and z∈V.

[F1]

A holomorphic logarithm branch L of z on V satisfies exp⁡(L(z))=z for every z∈V, and its branch power is zLα:=exp⁡(αL(z)) (Complex powers defined from a holomorphic logarithm branch).

[F2]

The complex integer powers satisfy z0=1, zm+1=zmz for m∈N, and zr:=(zm)−1 when r<0 with −r the natural m≥1 (Integer powers in the complex field).

[F3]

For all u,v∈C, exp⁡(u+v)=exp⁡u exp⁡v; for real x, the complex value exp⁡(x+0i) equals the real exponential ex (exp⁡(z+w)=exp⁡z exp⁡w, and the complex exponential extends the real exponential).

[F4]

The complex exponential is exp⁡z=∑n≥0zn/n! for every z∈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: zL0=exp⁡(0⋅L(z))=exp⁡0=1=z0

1.2ihassume-hyp

Assume for a fixed m≥0 that exp⁡(mL(z))=zm.

2.1F1F2F3step 1.2ih

By [F3] and [F1], exp⁡((m+1)L(z))=exp⁡(mL(z))exp⁡(L(z))=zmz=zm+1

3.1F2F3F4step 2.1

For r=−m<0: [F3] and [F4] give exp⁡(−mL(z))exp⁡(mL(z))=exp⁡0=1, so by step 2.1 and [F2], exp⁡(−mL(z))=(zm)−1=z−m=zr.

4.1step 2.1step 3.1discharge-induction∎

Steps 2.1 and 3.1 cover every integer, so zLn=zn; the right side mentions no branch, giving independence.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-29Open item page →

On positive reals, the principal branch power agrees with the published real power

Statement

For x>0 and real α∈R, the principal branch power xLog⁡α:=exp⁡(αLog⁡x) of Complex powers defined from a holomorphic logarithm branch equals the published real power xα of Real powers for positive bases, with the zero-base positive-exponent convention:

xLog⁡α=xα(x>0, α∈R).

Facts & Assumptions

Given: A positive real x>0 and a real exponent α∈R.

[F1]

On the slit plane, the principal branch power is zLog⁡α:=exp⁡(αLog⁡z), where Log⁡ is the holomorphic principal logarithm branch (Complex powers defined from a holomorphic logarithm branch).

[F2]

For a>0 and x∈R, the real power is ax:=exp⁡(xlog⁡a) (Real powers for positive bases, with the zero-base positive-exponent convention).

[F3]

For real x, the complex value exp⁡(x+0i) equals the published real exponential ex (exp⁡(z+w)=exp⁡z exp⁡w, and the complex exponential extends the real exponential).

Proof

technique · direct
1.1F1given

Log⁡x=log⁡x+i0, the real logarithm embedded in C: the polar form of x>0 uses angle 0.

2.1F1F2F3step 1.1algebra∎

Steps 1.1, [F1], [F3], and [F2] give xLog⁡α=exp⁡((αlog⁡x)+i0)=eαlog⁡x=xα.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-29Open item page →

Different branches shift logarithms by 2πik and complex powers by exponential factors

Statement

Let V⊆C be a connected open set with 0∉V, and let L1,L2:V→C be two holomorphic logarithm branches of z on V. There is a unique integer k∈Z with

L1(z)−L2(z)=2πikfor every z∈V.

Consequently, for every α∈C the branch powers of Complex powers defined from a holomorphic logarithm branch differ by

zL1α=e2πiαk zL2α(z∈V).

Additive and multiplicative branch laws are subject to exactly this discrepancy: a claimed identity log⁡(zw)=log⁡z+log⁡w or (zα)β=zαβ between branch values holds only after the relevant discrepancy vanishes on the points involved, and the companion page exhibits the principal-branch failures.

Facts & Assumptions

Given: A connected open V⊆C with 0∉V, and holomorphic logarithm branches L1,L2 of z on V; α∈C.

[F1]

A holomorphic logarithm branch L of z on V satisfies exp⁡(L(z))=z for every z∈V, and its branch power is zLα:=exp⁡(αL(z)) (Complex powers defined from a holomorphic logarithm branch).

[F2]
[F3]

For all u,v∈C, exp⁡(u+v)=exp⁡u exp⁡v (exp⁡(z+w)=exp⁡z exp⁡w, and the complex exponential extends the real exponential).

[F5]

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

Proof

technique · direct
1.1F1F2given

[F1] gives exp⁡(L1(z))=z=exp⁡(L2(z)); by [F2], L1(z)−L2(z)∈2πiZ.

2.1F4F5step 1.1

L1−L2 is continuous by [F5], so [F4] makes its image connected; step 1.1 gives one integer k with L1−L2≡2πik on V.

3.1F1F3step 2.1algebra∎

Substituting step 2.1 into [F1]: zL1α=exp⁡(αL2(z)+2πiαk)=e2πiαkexp⁡(αL2(z))=e2πiαkzL2α, using [F3] in the middle equality.

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-29Open item page →

Conformal equivalence and the automorphism group of a domain

Definition

Let U,V⊆C be complex domains. U and V are conformally equivalent when there exists a biholomorphism f:U→V in the sense of Biholomorphic maps between complex domains; such an f is then a conformal equivalence from U onto V.

For a complex domain U, the automorphism group of U is

Aut⁡(U):={ f:U→U:f is biholomorphic },

with composition as the group operation.

Why the group operation is legitimate. The identity map id⁡U is biholomorphic. If f is biholomorphic then its inverse f−1 is holomorphic by the definition of biholomorphy, so f−1∈Aut⁡(U) when f∈Aut⁡(U). If f,g∈Aut⁡(U) then the composite g∘f is biholomorphic: it is a bijection whose inverse f−1∘g−1 is a composite of holomorphic maps, hence holomorphic. Composition of maps is associative, so these three closure facts make Aut⁡(U) a group with identity id⁡U.

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-29Open item page →

The unit disc, the upper half-plane, and Blaschke factors

Definition

Fix the unit disc and the upper half-plane

D:={ z∈C:∣z∣<1 },H:={ z∈C:Im⁡z>0 },

using modulus and imaginary part of Real and imaginary parts, complex conjugation, and modulus.

For a∈D define the Blaschke factor

φa(z):=a−z1−a‾ z.

For every z with ∣z∣≤1, one has ∣a‾ z∣≤∣a∣<1, so the denominator never vanishes on the closed unit disc. Thus φa is holomorphic on an open disc containing the closed unit disc and in particular on D. Direct substitution records

φa(0)=a,φa(a)=0.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-29Open item page →

Blaschke factors are automorphisms of the disc

Statement

For each a∈D, the Blaschke factor

φa(z)=a−z1−a‾ z

is a biholomorphic self-map of D. More precisely,

φa(D)=Dandφa(φa(z))=z(z∈D),

so φa is an automorphism of the disc.

Facts & Assumptions

Given: A point a∈D.

[F1]

The unit disc is D={z∈C:∣z∣<1}, and the Blaschke factor is φa(z)=(a−z)/(1−a‾ z) with denominator nonzero on D (The unit disc, the upper half-plane, and Blaschke factors).

[F2]

A map between complex domains is biholomorphic exactly when it is bijective, holomorphic, and has holomorphic inverse (Biholomorphic maps between complex domains).

Proof

technique · direct
1.1F1givenalgebra

For z∈D, [F1] gives 1−∣φa(z)∣2=(∣1−a‾z∣2−∣a−z∣2)/∣1−a‾z∣2=(1−∣a∣2)(1−∣z∣2)/∣1−a‾z∣2>0, so ∣φa(z)∣<1 and φa(D)⊆D.

2.1F1step 1.1algebra

A direct simplification from [F1] gives φa(φa(z))=(a−a−z1−a‾z)/(1−a‾ a−z1−a‾z)=z for z∈D, so φa is its own inverse on D.

3.1F1F2step 2.1∎

By [F1], φa is holomorphic on D; step 2.1 makes it bijective with holomorphic inverse itself, so [F2] makes φa biholomorphic on D.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-29Open item page →

Schwarz lemma with the equality cases

Statement

Let f:D→D be holomorphic and satisfy f(0)=0. Then

∣f(z)∣≤∣z∣(z∈D),∣f′(0)∣≤1.

Moreover, if either ∣f(z0)∣=∣z0∣ for some z0∈D∖{0} or ∣f′(0)∣=1, then

f(z)=eiθz

for some real θ; conversely every rotation z↦eiθz satisfies equality in both conclusions.

Facts & Assumptions

Given: A holomorphic map f:D→D with f(0)=0.

[F1]

The unit disc is D={z∈C:∣z∣<1} (The unit disc, the upper half-plane, and Blaschke factors).

[F2]

If a holomorphic function on a punctured disc has a finite limit at the centre, then the singularity is removable (Characterizations of removable singularities).

[F3]

Boundary modulus control on a bounded domain bounds the modulus throughout the domain (Maximum modulus principle with boundary and infinity control).

[F4]

If the modulus of a holomorphic function has an interior local maximum, then the function is constant (Local maximum modulus principle).

Proof

technique · direct
1.1F1givencases

If f≡0 then the two inequalities and the equality characterization are immediate, so assume f is not identically zero and define g(z)=f(z)/z for z≠0 on the punctured disc.

2.1F2step 1.1algebra

Since f′(0)=lim⁡z→0f(z)/z, the function g has finite limit f′(0) at 0; by [F2] it extends holomorphically to D, still denoted g, with g(0)=f′(0).

3.1F1F3step 2.1algebra

Fix 0<r<1. On ∣z∣=r one has ∣g(z)∣=∣f(z)∣/r≤1/r because f(D)⊆D; applying [F3] on the radius-r disc gives ∣g(z)∣≤1/r whenever ∣z∣≤r.

4.1step 2.1step 3.1algebra

For any w∈D, step 3.1 holds for every r with ∣w∣<r<1, so letting r→1− gives ∣g(w)∣≤1; therefore ∣f(w)∣=∣w∣∣g(w)∣≤∣w∣ for all w∈D, and at w=0 this also gives ∣f′(0)∣=∣g(0)∣≤1.

5.1F4step 2.1step 4.1casesalgebra

If ∣f(z0)∣=∣z0∣ for some z0≠0, then step 4.1 gives ∣g(z0)∣=1, an interior maximum for ∣g∣, so [F4] makes g constant of modulus 1; if instead ∣f′(0)∣=1, then ∣g(0)∣=1 and the same argument applies. Thus in either equality case g(z)≡eiθ for some real θ, so f(z)=eiθz on D.

6.1step 5.1algebra∎

Conversely, for f(z)=eiθz one has ∣f(z)∣=∣z∣ for all z and ∣f′(0)∣=∣eiθ∣=1.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-29Open item page →

Schwarz-Pick lemma on the unit disc

Statement

Let f:D→D be holomorphic. Then for every a,z∈D,

∣f(z)−f(a)1−f(a)‾ f(z)∣≤∣z−a1−a‾ z∣.

Equivalently,

∣φf(a)(f(z))∣≤∣φa(z)∣.

Moreover,

∣f′(a)∣≤1−∣f(a)∣21−∣a∣2(a∈D),

and if equality holds for some distinct a,z∈D or in the derivative inequality at some a∈D, then f is an automorphism of D.

Facts & Assumptions

Given: A holomorphic self-map f:D→D and points a,z∈D.

[F1]

Every Blaschke factor φc is an automorphism of D (Blaschke factors are automorphisms of the disc).

[F2]

A disc self-map fixing 0 satisfies Schwarz's lemma, with equality only for rotations (Schwarz lemma with the equality cases).

[F3]

Holomorphic compositions satisfy the chain rule (The chain rule for complex derivatives).

Proof

technique · direct
1.1F1givenconstruct

Put b=f(a) and F=φb∘f∘φa. By [F1], the two Blaschke factors are disc automorphisms, so F:D→D is holomorphic and satisfies F(0)=φb(f(a))=0.

2.1F1F2step 1.1algebra

Applying [F2] to F at the point φa(z)∈D gives ∣F(φa(z))∣≤∣φa(z)∣, that is, ∣φb(f(z))∣≤∣φa(z)∣. This is exactly the displayed pseudohyperbolic inequality.

2.2F2F3step 1.1algebra

Since φa′(0)=∣a∣2−1 and φb′(b)=−1/(1−∣b∣2), the chain rule [F3] gives ∣F′(0)∣=∣φb′(b)∣ ∣f′(a)∣ ∣φa′(0)∣=(1−∣a∣2)∣f′(a)∣/(1−∣b∣2). Applying the derivative part of [F2] to F yields the stated bound for ∣f′(a)∣.

3.1F1F2step 2.1step 2.2casesalgebra∎

If equality holds in the pseudohyperbolic inequality for some z≠a, then equality holds in Schwarz's lemma for F at the nonzero point φa(z); if equality holds in the derivative inequality, then ∣F′(0)∣=1. In either case [F2] makes F a rotation, so f=φb∘F∘φa is an automorphism by [F1].

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-29Open item page →

Every automorphism of the disc is a rotated Blaschke factor

Statement

A holomorphic map f:D→D is an automorphism of D if and only if there exist a∈D and θ∈R such that

f(z)=eiθφa(z)=eiθa−z1−a‾ z(z∈D).

Facts & Assumptions

Given: A holomorphic self-map f:D→D.

[F1]

The automorphism group Aut⁡(D) consists of the biholomorphic self-maps of D (Conformal equivalence and the automorphism group of a domain).

[F2]

Every Blaschke factor is an automorphism of D (Blaschke factors are automorphisms of the disc).

[F3]

Equality in Schwarz's lemma characterizes rotations (Schwarz lemma with the equality cases).

Proof

technique · direct
1.1F1F2givenconstruct

Assume first that f∈Aut⁡(D), and let a=f−1(0). By [F2], the map g:=f∘φa is an automorphism of D with g(0)=0.

2.1F1F3step 1.1algebra

Applying [F3] to g and to its inverse g−1 shows ∣g(z)∣≤∣z∣ and ∣z∣=∣g−1(g(z))∣≤∣g(z)∣ for every z∈D, so ∣g(z)∣=∣z∣ throughout D. Hence [F3] forces g(z)=eiθz for some real θ.

3.1F1F2step 2.1algebra∎

Therefore f(z)=g(φa(z))=eiθφa(z). Conversely, if f(z)=eiθφa(z), then the rotation z↦eiθz and the Blaschke factor φa are automorphisms, so [F2] and [F1] make f an automorphism.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-29Open item page →

Automorphisms of the upper half-plane are real Mobius maps

Statement

A map f:H→H is an automorphism of the upper half-plane if and only if

f(z)=az+bcz+d

for real numbers a,b,c,d with ad−bc>0.

Facts & Assumptions

Given: The upper half-plane H={z∈C:Im⁡z>0}.

[F1]

Automorphisms are biholomorphic self-maps in the sense of Conformal equivalence and the automorphism group of a domain.

[F2]

Every disc automorphism is a rotated Blaschke factor (Every automorphism of the disc is a rotated Blaschke factor).

[F3]

Every Möbius transformation is a biholomorphism of the Riemann sphere (Every Möbius transformation is a biholomorphism of the Riemann sphere).

[F4]

A Möbius transformation has the form (az+b)/(cz+d) with ad−bc≠0 (Möbius transformations of the Riemann sphere).

Proof

technique · direct
1.1F3F4givenalgebra

The Cayley transform C(z)=(z−i)/(z+i) is Möbius by [F4], hence biholomorphic by [F3]; the identities ∣z+i∣2−∣z−i∣2=4Im⁡z and C−1(ζ)=i(1+ζ)/(1−ζ) show that C maps H biholomorphically onto D.

2.1F1F4step 1.1givenconstruct

Assume f∈Aut⁡(H). Let α=f−1(i)=u+iv with v>0, and define m(z)=(z−u)/v; this is a real Möbius automorphism of H with m(α)=i, so h:=f∘m−1 is an automorphism of H fixing i.

3.1F2F3F4step 1.1step 2.1algebra

The map G:=C∘h∘C−1 is an automorphism of D fixing 0, so [F2] gives G(ζ)=eiθζ for some real θ. Conjugating back and simplifying with 1±eiθ=2eiθ/2(cos⁡(θ/2)∓isin⁡(θ/2)) gives h(z)=(cos⁡(θ/2)z+sin⁡(θ/2))/(−sin⁡(θ/2)z+cos⁡(θ/2)), which has real coefficients and determinant 1; since m also has real coefficients and positive determinant v, the composition f=h∘m is a real Möbius map with positive determinant.

4.1F1F4algebra∎

Conversely, if f(z)=(az+b)/(cz+d) with a,b,c,d∈R and ad−bc>0, then Im⁡f(z)=((ad−bc)Im⁡z)/∣cz+d∣2>0 for z∈H, so f[H]⊆H; its inverse (dz−b)/(−cz+a) has the same form with real coefficients and positive determinant, so f∈Aut⁡(H).

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-29Open item page →

The Poincare metric and distance on the unit disc

Definition

On the unit disc D of The unit disc, the upper half-plane, and Blaschke factors fix the Poincare metric, also called the hyperbolic metric of the disc,

dsD:=2 ∣dz∣1−∣z∣2.

For a piecewise C1 curve γ:[a,b]→D its Poincare length is

ℓD(γ):=∫γ2 ∣dz∣1−∣z∣2=∫ab2 ∣γ′(t)∣1−∣γ(t)∣2 dt,

and the Poincare distance between z,w∈D is

dD(z,w):=inf⁡{ ℓD(γ):γ a piecewise C1 curve in D from z to w }.

The image of γ is a compact subset of D, so 1−∣γ(t)∣2 is bounded away from 0. On each of the finitely many C1 pieces, ∣γ′(t)∣ is continuous and bounded; hence the displayed integrand is piecewise continuous and integrable, and each ℓD(γ) is a finite real number. The infimum is taken over a nonempty set, because D is convex and the segment from z to w lies in D. This normalisation — factor 2, curvature −1 — is fixed for every later surface page. The explicit formula dD(z,w)=2artanh⁡∣φz(w)∣ and the metric axioms are established on this page by the Poincare-distance formula theorem; the present definition records the intrinsic path-metric construction it evaluates.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-29Open item page →

The Poincare distance has the formula 2artanh⁡∣φz(w)∣ and is disc-automorphism invariant

Statement

For z,w∈D, the Poincare distance on the unit disc satisfies

dD(z,w)=2artanh⁡∣φz(w)∣,

where φz is the Blaschke factor carrying z to 0. Moreover every disc automorphism preserves this distance.

Facts & Assumptions

Given: The Poincare metric and distance on D.

[F1]

The Poincare length and distance are defined by integrating 2∣dz∣/(1−∣z∣2) along piecewise C1 curves (The Poincare metric and distance on the unit disc).

[F2]

Every Blaschke factor is an automorphism of D (Blaschke factors are automorphisms of the disc).

[F3]

Every automorphism of D is a rotated Blaschke factor (Every automorphism of the disc is a rotated Blaschke factor).

Proof

technique · direct
1.1F1F2givenalgebra

For a Blaschke factor φa, a direct differentiation gives φa′(z)=−(1−∣a∣2)/(1−a‾z)2 and 1−∣φa(z)∣2=(1−∣a∣2)(1−∣z∣2)/∣1−a‾z∣2. Therefore 2∣φa′(z)∣/(1−∣φa(z)∣2)=2/(1−∣z∣2), so φa preserves Poincare length of every piecewise C1 curve.

2.1F1F2F3step 1.1algebra

Since length is preserved under φa, taking infima in [F1] gives dD(φa(z),φa(w))=dD(z,w). By [F3], every disc automorphism is a composition of a Blaschke factor and a rotation, and rotations satisfy the same identity, so every disc automorphism preserves dD.

3.1F1step 2.1algebra

By step 2.1, dD(z,w)=dD(0,φz(w)). Write r=∣φz(w)∣. If r=0, then φz(w)=0, so z=w and both sides are 0=2artanh⁡0. If r>0, the radial segment γ(t)=t φz(w)/r from 0 to φz(w) has Poincare length ∫0r2 dt/(1−t2)=2artanh⁡r, so dD(0,φz(w))≤2artanh⁡r.

4.1F1step 3.1algebra

For any piecewise C1 curve γ from 0 to φz(w), one has ∣(∣γ∣)′∣≤∣γ′∣, hence ℓD(γ)≥∫2∣(∣γ∣)′∣/(1−∣γ∣2) dt≥∫0r2 ds/(1−s2)=2artanh⁡r. Taking the infimum over all such curves gives the reverse inequality.

5.1step 2.1step 3.1step 4.1∎

Combining steps 3.1 and 4.1 yields dD(z,w)=2artanh⁡∣φz(w)∣, and step 2.1 gives automorphism invariance.

RemarkRemark: AI-adaptedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-29Open item page →

Biholomorphisms are conformal and have holomorphic inverse

Remark

A biholomorphism is holomorphic and has a holomorphic inverse by Biholomorphic maps between complex domains, so it is conformal in the orientation-preserving sense this page uses: holomorphic with nowhere-vanishing derivative. The derivative cannot vanish at any point of its domain, because the local inverse supplied by Holomorphic inverse function theorem and local-degree criterion has derivative g′(w)=1/f′(g(w)); a vanishing f′ would make that expression undefined. Such a map preserves the magnitude and the orientation of angles between tangent directions at every point.

The convention here is deliberately orientation-sensitive: complex conjugation z↦z‾ preserves angle magnitudes but reverses orientation, so it is not conformal in this library's sense. That exclusion is exercised by the companion page's conjugation counterexample.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-29Open item page →

Conformal equivalence is an equivalence relation

Statement

Conformal equivalence of complex domains is an equivalence relation: every complex domain U is conformally equivalent to itself; if U is conformally equivalent to V then V is conformally equivalent to U; and if U is conformally equivalent to V and V to W, then U is conformally equivalent to W.

Facts & Assumptions

Given: Complex domains U,V,W, and the conformal-equivalence notion of Conformal equivalence and the automorphism group of a domain.

[F1]

U and V are conformally equivalent when there exists a biholomorphism f:U→V. The identity map id⁡U is biholomorphic; the inverse of a biholomorphism is biholomorphic; and the composite of two biholomorphisms U→U is biholomorphic (Conformal equivalence and the automorphism group of a domain).

Proof

technique · direct
1.1F1given

Reflexivity: [F1] makes id⁡U biholomorphic, witnessing U∼U.

1.2F1assume-hyp

Symmetry: for biholomorphic f:U→V, [F1] makes f−1:V→U biholomorphic.

1.3F1assume-hyp

Transitivity: for biholomorphic f:U→V, g:V→W, [F1] makes g∘f biholomorphic.

2.1step 1.1step 1.2step 1.3∎

Steps 1.1-1.3 are the three clauses of an equivalence relation.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-29Open item page →

Power maps are biholomorphisms on sectors of width less than 2π/n

Statement

Let n≥1 be an integer, let α<β be real numbers with β−α<2π/n, and define

S:={ reiθ:r>0, α<θ<β },T:={ ρeiϕ:ρ>0, nα<ϕ<nβ }.

Then the power map f(z)=zn is a biholomorphism from S onto T.

Facts & Assumptions

Given: The integer n≥1 and the sectors S,T above.

[F1]

On the slit plane the principal logarithm is holomorphic and satisfies exp⁡(Log⁡z)=z (The principal logarithm is the normalised holomorphic branch on the slit plane).

[F2]

If L is a holomorphic logarithm branch on a domain, then zLα:=exp⁡(αL(z)) defines the branch power (Complex powers defined from a holomorphic logarithm branch).

[F3]

For integer exponents, branch powers agree with ordinary powers (Branch-defined complex powers agree with integer powers).

[F5]

A map is biholomorphic when it is bijective, holomorphic, and has holomorphic inverse (Biholomorphic maps between complex domains).

Proof

technique · direct
1.1F1givenconstruct

Put γ=(α+β)/2 and δ=(β−α)/2, so δ<π/n≤π; if z∈S then e−iγz has argument in (−δ,δ)⊂(−π,π), so L(z):=Log⁡(e−iγz)+iγ is a holomorphic logarithm branch on S by [F1].

2.1F2F3F4step 1.1algebra

By [F2] and [F3], f(z)=zn=exp⁡(nL(z)) on S, so f is holomorphic there; moreover arg⁡f(z)=narg⁡z with narg⁡z∈(nα,nβ), hence f[S]⊆T.

2.2F1F4step 1.1constructalgebra

If w∈T, then e−inγw has argument in (−nδ,nδ)⊂(−π,π), so M(w):=Log⁡(e−inγw)+inγ is a holomorphic logarithm branch on T by [F1]; define g(w):=exp⁡(M(w)/n). Then g is holomorphic on T, arg⁡g(w)∈(α,β), and g[T]⊆S.

3.1F2F3F5step 2.1step 2.2algebra∎

By [F2] and [F3], g(w)n=exp⁡(M(w))=w for w∈T, while for z∈S one has g(f(z))=exp⁡(nL(z)/n)=z because nL(z) has imaginary part in (nα,nβ) and so is the chosen branch value M(f(z)). Therefore g=f−1, and [F5] makes f biholomorphic from S onto T.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-29Open item page →

A slit-plane root branch biholomorphically parametrizes a sector

Statement

Let n≥1 be an integer, let

S:=C∖{x∈R:x≤0},Vn:={ reiθ:r>0, −π/n<θ<π/n },

and define

Rn(z):=exp⁡ ⁣(Log⁡zn)(z∈S).

Then Rn is a biholomorphism from S onto Vn, and its inverse is the power map w↦wn on Vn.

Facts & Assumptions

Given: The integer n≥1, the slit plane S, and the map Rn above.

[F1]

The principal logarithm is holomorphic on S and satisfies exp⁡(Log⁡z)=z (The principal logarithm is the normalised holomorphic branch on the slit plane).

[F2]

Branch powers are defined by zLα=exp⁡(αL(z)) (Complex powers defined from a holomorphic logarithm branch).

[F3]

For integer exponents, branch powers agree with ordinary powers (Branch-defined complex powers agree with integer powers).

[F4]

A map is biholomorphic when it is bijective, holomorphic, and has holomorphic inverse (Biholomorphic maps between complex domains).

Proof

technique · direct
1.1F1givenalgebra

Since Log⁡ is holomorphic on S by [F1], the map Rn(z)=exp⁡(Log⁡z/n) is holomorphic on S; if z=reiθ with −π<θ<π, then arg⁡Rn(z)=θ/n∈(−π/n,π/n), so Rn[S]⊆Vn.

2.1F1step 1.1algebra

If w∈Vn, write w=reiθ with r>0 and −π/n<θ<π/n. Then wn=rneinθ lies in S because nθ∈(−π,π), and the principal logarithm of wn is Log⁡(wn)=log⁡(rn)+inθ=n(log⁡r+iθ). Therefore Rn(wn)=exp⁡ ⁣(Log⁡(wn)n)=exp⁡(log⁡r+iθ)=w.

3.1F1F2F3F4step 2.1algebra∎

For z∈S, [F2] with [F3] gives (Rn(z))n=exp⁡(Log⁡z)=z by [F1], so the inverse of Rn on Vn is w↦wn. Therefore [F4] makes Rn:S→Vn biholomorphic.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-29Open item page →

The principal logarithm is a biholomorphism from the slit plane to the principal strip

Statement

Let

S:=C∖{x∈R:x≤0},P:={ w∈C:−π<Im⁡w<π }.

Then the principal logarithm

Log⁡:S→P

is a biholomorphism.

Facts & Assumptions

Given: The slit plane S and the principal strip P above.

[F1]

On S, the principal logarithm is holomorphic, satisfies exp⁡(Log⁡z)=z, and has imaginary part in (−π,π) (The principal logarithm is the normalised holomorphic branch on the slit plane).

[F2]

The dictionary remark distinguishes the holomorphic principal branch on S from the pointwise boundary value on the negative axis (Dictionary for holomorphic logarithm branches, the principal logarithm, and principal powers).

[F4]
[F5]

A map is biholomorphic when it is bijective, holomorphic, and has holomorphic inverse (Biholomorphic maps between complex domains).

Proof

technique · direct
1.1F1F2given

By [F1] and [F2], Log⁡ is holomorphic on S and maps S into P.

2.1F1step 1.1algebra

If Log⁡z1=Log⁡z2, then exponentiating and using [F1] gives z1=exp⁡(Log⁡z1)=exp⁡(Log⁡z2)=z2. Thus Log⁡ is injective.

3.1F1F4step 2.1algebra

If w=u+iv∈P, then [F4] gives exp⁡w=eu(cos⁡v+isin⁡v)≠0; because v∈(−π,π), this value is never on the nonpositive real axis, so exp⁡w∈S, and its principal logarithm is exactly w. Hence Log⁡ is surjective onto P with inverse w↦exp⁡w.

4.1F3F5step 1.1step 3.1∎

The inverse w↦exp⁡w is holomorphic by [F3]. Therefore [F5] makes Log⁡:S→P a biholomorphism.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-29Open item page →

The exponential is the inverse biholomorphism from the principal strip to the slit plane

Statement

Let

P:={ w∈C:−π<Im⁡w<π },S:=C∖{x∈R:x≤0}.

Then the restriction

exp⁡:P→S

is a biholomorphism, and its inverse is the principal logarithm.

Facts & Assumptions

Given: The principal strip P and slit plane S above.

[F1]

The principal logarithm is a biholomorphism Log⁡:S→P (The principal logarithm is a biholomorphism from the slit plane to the principal strip).

[F3]

A map is biholomorphic when it is bijective, holomorphic, and has holomorphic inverse (Biholomorphic maps between complex domains).

Proof

technique · direct
1.1F1given

By [F1], every z∈S satisfies Log⁡z∈P and exp⁡(Log⁡z)=z, so exp⁡:P→S is surjective and Log⁡ is a two-sided inverse candidate.

2.1F1step 1.1algebra

If w∈P, then [F1] applied to z=exp⁡w∈S gives Log⁡(exp⁡w)=w, so exp⁡ is injective on P.

3.1F1F2F3step 1.1step 2.1∎

The restriction of exp⁡ to P is holomorphic by [F2], and its inverse is the holomorphic map Log⁡ by [F1]. Therefore [F3] makes exp⁡:P→S biholomorphic.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-29Open item page →

The Joukowski map is a biholomorphism from the exterior disc onto C∖[−1,1]

Statement

Let

E:={z∈C:∣z∣>1},Ω:=C∖[−1,1],

and define the Joukowski map by

J(z):=12(z+1z)(z∈E).

Then J:E→Ω is a biholomorphism.

Facts & Assumptions

Given: The exterior disc E, the slit-complement Ω, and the map J above.

[F1]

For n=2, the slit-plane root branch R2(t)=exp⁡(Log⁡t/2) is a biholomorphism from C∖{x∈R:x≤0} onto the right half-plane {s∈C:Re⁡s>0}, with inverse s↦s2 (A slit-plane root branch biholomorphically parametrizes a sector).

Proof

technique · direct
1.1F1givenconstructalgebra

For w∈Ω, put m(w):=(w−1)/(w+1). If m(w) were a nonpositive real number, then w=(1+m(w))/(1−m(w)) would lie in [−1,1], contradicting w∈Ω; also m(w)≠1 because (w−1)/(w+1)=1 has no finite solution. Hence m maps Ω holomorphically into the slit plane of [F1]. Define s(w):=R2(m(w)), so Re⁡s(w)>0 for every w∈Ω.

2.1F1step 1.1algebra

Define H(w):=(1+s(w))/(1−s(w)) on Ω. Since s(w)≠1, this is holomorphic there; using s(w)2=m(w) gives J(H(w))=12(1+s1−s+1−s1+s)=1+s21−s2=1+m(w)1−m(w)=w, and ∣1+s(w)∣2−∣1−s(w)∣2=4Re⁡s(w)>0 yields ∣H(w)∣>1, so H(Ω)⊆E.

3.1F1step 2.1algebra

For z∈E, put s:=(z−1)/(z+1). Then Re⁡s=(∣z∣2−1)/∣z+1∣2>0, so s lies in the right half-plane, and a direct calculation gives (J(z)−1)/(J(z)+1)=((z−1)/(z+1))2=s2. By [F1], the right-half-plane inverse of squaring is exactly R2, so R2((J(z)−1)/(J(z)+1))=s, and substituting this into the definition of H yields H(J(z))=(1+s)/(1−s)=z.

4.1step 2.1step 3.1∎

Steps 2.1 and 3.1 show that J and H are holomorphic two-sided inverses between E and Ω. Therefore J:E→Ω is a biholomorphism.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-29Open item page →

The sine map biholomorphically sends an upper half-strip onto the upper half-plane

Statement

Let

S:={ z∈C:−π/2<Re⁡z<π/2, Im⁡z>0 }.

Then the sine map

sin⁡:S→H

is a biholomorphism onto the upper half-plane H={w∈C:Im⁡w>0}.

Facts & Assumptions

Given: The upper half-strip S above.

[F1]

The exponential is a biholomorphism from the principal strip P={u∈C:−π<Im⁡u<π} onto the slit plane C∖{x∈R:x≤0}, with inverse the principal logarithm (The exponential is the inverse biholomorphism from the principal strip to the slit plane).

[F2]

The Joukowski map J(η)=12(η+η−1) is a biholomorphism from {∣η∣>1} onto C∖[−1,1] (The Joukowski map is a biholomorphism from the exterior disc onto C∖[−1,1]).

[F3]

Complex sine is defined by sin⁡z=exp⁡(iz)−exp⁡(−iz)2i (Complex sine, cosine, hyperbolic sine, and hyperbolic cosine from the complex exponential).

Proof

technique · direct
1.1F1givenconstructalgebra

Fix z∈S and put q:=exp⁡(iz). Since iz has real part −Im⁡z<0 and imaginary part Re⁡z∈(−π/2,π/2)⊂(−π,π), [F1] gives q in the slit plane with ∣q∣<1 and Re⁡q>0. Define η:=−i/q; then ∣η∣>1 and Im⁡η=−Re⁡q/∣q∣2<0.

2.1F2F3step 1.1algebra

By [F3], sin⁡z=(q−q−1)/(2i)=−(η+η−1)/2=−J(η). For η=u+iv with ∣η∣>1, one has Im⁡J(η)=12(v−vu2+v2)=v2(1−1∣η∣2), so step 1.1 gives Im⁡J(η)<0 and therefore Im⁡sin⁡z>0. Hence sin⁡[S]⊆H.

3.1F1F2step 2.1givenconstructalgebra

Conversely, let w∈H. Since −w∈C∖[−1,1], [F2] supplies a unique η∈{∣η∣>1} with J(η)=−w. The imaginary-part formula from step 2.1 shows Im⁡η has the same sign as Im⁡J(η)=−Im⁡w<0, so Im⁡η<0. Put q:=−i/η; then ∣q∣<1 and Re⁡q=−Im⁡η/∣η∣2>0, so q lies in the right half-disc. By [F1], u:=Log⁡q belongs to the principal strip, with Re⁡u=log⁡∣q∣<0 and Im⁡u∈(−π/2,π/2). Therefore z:=−iu lies in S.

4.1F1F2F3step 3.1algebra

For the point z of step 3.1, [F1] gives exp⁡(iz)=q, so the identity of step 2.1 yields sin⁡z=−J(−i/q)=−J(η)=w. Thus sin⁡:S→H is surjective.

5.1F1F2F3step 3.1step 4.1∎

If z1,z2∈S and sin⁡z1=sin⁡z2, step 2.1 gives J(η1)=J(η2) for ηj:=−iexp⁡(−izj). By [F2], η1=η2, so exp⁡(iz1)=exp⁡(iz2). Because each izj lies in the principal strip, [F1] makes the exponential injective there, and hence z1=z2. Therefore sin⁡ is bijective. Its inverse is the holomorphic composition w↦−iLog⁡(−i/K(−w)), where K is the holomorphic inverse supplied by [F2]. Thus sin⁡:S→H is a biholomorphism.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-29Open item page →

The sphere, the plane, and the disc are pairwise non-biholomorphic

Statement

The Riemann sphere C^, the complex plane C, and the unit disc D are pairwise non-biholomorphic.

Facts & Assumptions

Given: The three domains C^, C, and D.

[F1]

A conformal equivalence is a biholomorphism between domains (Conformal equivalence and the automorphism group of a domain).

[F3]

Every bounded entire function is constant (Liouville's theorem: every bounded entire function is constant).

Proof

technique · direct
1.1F1F2given

If there were a biholomorphism from C^ onto C or onto D, then [F2] would make the target compact because C^ is compact, but neither C nor D is compact. Hence the sphere is biholomorphic to neither the plane nor the disc.

1.2F1F3algebra

If there were a biholomorphism f:C→D, then f would be a bounded entire function and [F3] would make it constant, contradicting bijectivity. Hence C and D are not biholomorphic.

2.1step 1.1step 1.2∎

Steps 1.1 and 1.2 cover all three pairs, so C^, C, and D are pairwise non-biholomorphic.

5 · Examples, counterexamples and false statements

None yet.

Sources