Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-26
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.

The winding number vanishes on the unbounded component of the complement of the trace

Statement

Let γ be a closed complex contour with trace γ∗ and length L(γ). Then C∖γ∗ has exactly one unbounded connected component U∞, and

n(γ,p)=0for every p∈U∞.

More precisely, if R>0 satisfies γ∗⊆{z:∣z∣≤R} and ∣p∣>R+L(γ)/(2π), then p∈U∞ and n(γ,p)=0.

Facts & Assumptions

Given: A closed complex contour γ:[a,b]→C.

[L1]

For a compact K⊆C, the complement C∖K has exactly one unbounded connected component U∞, every other component is bounded, and {z:∣z∣>R}⊆U∞ whenever R>0 satisfies K⊆{z:∣z∣≤R} (The complement of a compact plane set has exactly one unbounded connected component).

[L2]

The index n(γ,⋅) is constant on every connected component of C∖γ∗ (The winding number is constant on each connected component of the complement of the trace).

[L3]

The winding number of a closed complex contour about a point off its trace is an integer (The winding number of a closed contour is an integer).

[L4]

If ∣f(z)∣≤M on the trace of a rectifiable contour γ, with M≥0, then ∣∫γf(z) dz∣≤M L(γ) (ML estimate: a contour integral is bounded by a supremum bound times path length).

[L5]

n(γ,p)=(2πi)−1∫γdz/(z−p) (The winding number of a closed contour about a point off its trace).

[L7]

The connected component C(x) is the union of all connected subsets containing x (Connected components, quasicomponents, and totally disconnected spaces) and contains every connected subset containing x (The components of a space are its maximal connected subsets, they partition it, and each of them is closed).

[L8]

A subset of a metric space is bounded when it is empty or contained in some ball (Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space).

[L10]

The integers form an ordered commutative ring and their canonical image in R is discrete; in particular the only integer of modulus below 1 is 0 (The integers form a commutative ring, The integers form a totally ordered ring, Integer part: for every real x there is exactly one integer m with m≤x<m+1).

Proof

technique · direct
1.1givenL1L6L8

The trace γ∗ is the continuous image of a compact interval, hence compact by [L6], and bounded by [L6], so there is R>0 with γ∗⊆{z:∣z∣≤R}. By [L1] the set C∖γ∗ has exactly one unbounded component U∞, and {z:∣z∣>R}⊆U∞.

2.1step 1.1L4L5L9

Let ∣p∣>R. For w∈γ∗ one has ∣w∣≤R, so ∣w−p∣≥∣p∣−∣w∣≥∣p∣−R>0 by [L9]; hence p∉γ∗ and ∣1/(z−p)∣≤1/(∣p∣−R) on the trace. By [L4] and [L5], ∣n(γ,p)∣≤L(γ)/(2π(∣p∣−R)).

3.1step 1.1step 2.1L3L10

If in addition ∣p∣>R+L(γ)/(2π) then ∣p∣−R>L(γ)/(2π), so step 2.1 gives ∣n(γ,p)∣<1; since n(γ,p) is an integer by [L3], it is 0 by [L10]. Such p exist, for instance p=R+L(γ)/(2π)+1, and each lies in U∞ by step 1.1.

4.1step 3.1L2L7∎

By [L2] the index is constant on the connected component U∞, and step 3.1 exhibits a point of U∞ where its value is 0; hence n(γ,p)=0 for every p∈U∞, which by [L7] contains every connected unbounded subset of C∖γ∗ that meets it.

Depends on

Used by

Dependency tree · two levels

113 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