Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-27
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 boundary point whose complementary component contains another point is regular

Statement

Let ΩC be a bounded complex domain and let ζΩ. If the connected component of C^Ω containing ζ also contains a second point, then ζ is regular for Ω.

Facts & Assumptions

Given: A bounded complex domain Ω, a boundary point ζΩ, and a second point in the same connected component of C^Ω as ζ.

[L1]

For a cycle, the index is locally constant off the trace and vanishes on every connected set in the zero-index region that meets infinity (The index of a cycle is locally constant off its trace and vanishes far from it).

[L2]

A complex domain is homologically simply connected exactly when every cycle with trace in it is null-homologous there, equivalently when every holomorphic nowhere-zero function on it has a holomorphic logarithm (Null-homologous cycles and homologous cycles in an open set, Equivalent characterisations of a homologically simply connected domain).

[L3]

Harmonicity is preserved by holomorphic changes of coordinate (Plane harmonicity is preserved by holomorphic and antiholomorphic changes of coordinate).

[L4]

A weak local subharmonic peak function implies regularity (A weak local subharmonic peak function upgrades to regularity).

Proof

technique · direct
1.1

Let aζ lie in the same connected component E of C^Ω as ζ, and let [given, construct] T(w)=wζwa. This Möbius map sends ζ to 0, sends a to , and maps Ω biholomorphically onto the domain Ω=T(Ω). Its image E=T(E) is a connected subset of C^Ω containing both 0 and . Put G=C^E. Then G is an open connected neighbourhood of Ω and 0G.

givenconstruct
2.1

Let Γ be any cycle whose trace lies in G. By [L1], the index n(Γ,) is locally constant on CΓ and vanishes on the unbounded zero-index region. The connected set EC is disjoint from Γ, and because E also contains , the local constancy from [L1] forces n(Γ,p)=0 for every pEC. Since E=C^G, this says exactly that Γ is null-homologous in G by [L2]. Therefore G is homologically simply connected.

L1L2step 1.1
2.2

Because G is homologically simply connected and misses 0, [L2] gives a holomorphic logarithm L of the identity map on G, so exp(L(w))=w for wG. Hence [L2, step 1.1, construct] ReL(w)=logw. Because T(z)0 as zζ through Ω and 0Ω, choose a small neighbourhood V of 0 with ΩV{0<w<1}. On ΩV the function q(w)=Re1L(w) is harmonic, negative, and tends to 0 as w0 through Ω, because ReL(w)=logw. So q is a weak local harmonic peak function at 0 for the domain Ω.

L2step 1.1construct
3.1

The composition qT is harmonic on ΩT1(V) by [L3], is negative there, and tends to 0 as zζ through Ω. Thus qT is a weak local subharmonic peak function at ζ. Applying [L4] shows that ζ is regular for Ω.

L3L4step 2.2

Depends on

Used by

Dependency tree · two levels

51 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