Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-31
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 homologically simply connected plane domain has connected spherical complement

Statement

Let ΩC be a homologically simply connected complex domain. Then C^Ω is connected.

Facts & Assumptions

Given: A homologically simply connected complex domain Ω.

[L1]

A homologically simply connected complex domain is a complex domain in which every cycle with trace in the domain has index 0 at every omitted point (Homologically simply connected complex domains, A complex domain is a nonempty connected open subset of C).

[L2]

A compact subset of an open Euclidean set lies in the interior of a compact Jordan set contained in that open set, and that Jordan set may be chosen as a finite union of closed grid rectangles (A compact subset of an open Euclidean set has a compact Jordan neighborhood inside that open set).

[L3]

Chain integrals and indices are additive in the chain, reversing orientation negates the index, and a sum of cycles is a cycle (Chain integration and the index are additive in the chain, and reverse with it).

[L4]

For a closed contour, the winding number about a point off the trace equals the increment of a continuous argument divided by 2π (The winding number is the increment of a continuous argument divided by 2π).

[L5]

The index of a cycle is locally constant off its trace (The index of a cycle is locally constant off its trace and vanishes far from it).

Proof

technique · direct
1.1

Suppose, toward a contradiction, that F:=C^Ω is disconnected. Then F=AB for disjoint nonempty closed subsets A,BF. Since F, relabel so that B. Because the Riemann sphere is a metric space, the disjoint closed sets A and B have disjoint open neighbourhoods U and V in C^ with AU and BV. The inclusion V forces UC, so A is compact in C and U(CΩ)=UF=A. Hence UAΩ.

givenconstructassume-contra
2.1

Apply [L2] to the compact set AU, viewing C as R2. It gives a finite union J of closed grid rectangles with AintJJU. Give each rectangle boundary its positive orientation, sum those boundary chains, and cancel every interior edge with its opposite by [L3]. Let Γ be the remaining chain. Then Γ is a cycle, and its trace is the frontier of J, so ΓUAΩ.

step 1.1L2L3construct
3.1

Let pintJ lie on no grid line. Exactly one grid cell Q of J contains p. Along the positively oriented boundary of Q, the continuous argument of ζp increases by 2π, while along the boundary of every other grid cell it has increment 0 because p lies outside that cell. Therefore [L4] gives winding number 1 for +Q about p and 0 for every other cell boundary, and additivity from [L3] yields n(Γ,p)=1.

step 2.1L3L4algebra
4.1

Fix aA. Because AintJ, choose a disc D(a,r)intJ and then choose pD(a,r) on no grid line. The disc misses Γ, so local constancy from [L5] and step 3.1 give n(Γ,a)=n(Γ,p)=1.

step 2.1step 3.1L5choose
5.1

The point a lies in CΩ, while step 2.1 gives ΓΩ. Step 4.1 yields n(Γ,a)=10, so [L1] says that Γ is not null-homologous in Ω, contradicting the homological simple connectivity of Ω. Therefore the assumption of step 1.1 was false, and C^Ω is connected.

step 2.1step 4.1L1discharge-contradiction

Depends on

Used by

Dependency tree · two levels

54 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