Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-30
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 proper homologically simply connected plane domain has a bounded univalent competitor

Statement

Let ΩC be homologically simply connected and let z0Ω. Then the extremal family F(Ω,z0) is nonempty.

Facts & Assumptions

Given: A proper homologically simply connected complex domain ΩC and a point z0Ω.

[L1]

On a homologically simply connected complex domain, every holomorphic nowhere-zero function has a holomorphic square root (A nonvanishing holomorphic function on such a domain has holomorphic roots of every positive order).

[L2]

For each aD, the Blaschke factor φa is a biholomorphic self-map of D (Blaschke factors are automorphisms of the disc).

[L3]

A nonconstant holomorphic map on a domain has open image (Open mapping theorem for holomorphic functions).

Proof

technique · direct
1.1

Because ΩC, choose aCΩ. The function zza is holomorphic and nowhere zero on Ω, so [L1] gives a holomorphic q:ΩC with q(z)2=za.

L1givenchoose
2.1

If q(z1)=q(z2) then z1a=q(z1)2=q(z2)2=z2a, so z1=z2; thus q is injective. Also 0q(Ω), and q(Ω)(q(Ω))= because q(z1)=q(z2) would again force z1=z2, hence q(z1)=0, impossible.

step 1.1algebra
3.1

Put w0:=q(z0). Since q is nonconstant, [L3] makes q(Ω) open, so choose ρ>0 with D(w0,ρ)q(Ω). Step 2.1 gives q(Ω)(q(Ω))=, hence D(w0,ρ)=D(w0,ρ)q(Ω) is disjoint from q(Ω). Therefore q(z)+w0ρ for every zΩ.

L3step 2.1choose
4.1

Define h(z):=ρ2(q(z)+w0). Step 3.1 gives h(z)1/2, so h(Ω)D. The reciprocal affine map is injective away from w0, and step 2.1 makes q injective, so h is holomorphic and injective on Ω.

step 2.1step 3.1algebra
5.1

Let b=h(z0)D. By [L2], g:=φbh is holomorphic and injective from Ω into D, and g(z0)=0. Differentiating q2=za gives q(z0)=1/(2w0)0, so g(z0)0. Multiplying by the unimodular constant g(z0)/g(z0) makes the derivative at z0 positive. The resulting map lies in F(Ω,z0).

L2step 1.1step 4.1algebra

Depends on

Used by

Dependency tree · two levels

26 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