Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 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 of a closed contour is an integer

Statement

Let γ:[a,b]→C be a closed complex contour and let p∈C with p∉γ∗. Then

n(γ,p)=12πi∫γdzz−p∈Z.

No differentiability of γ is used: the contour is only assumed rectifiable.

Facts & Assumptions

Given: A closed complex contour γ:[a,b]→C and a point p∉γ∗.

[L1]

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

[L2]

For a complex contour γ:[a,b]→C, a point p∉γ∗ and a continuous logarithm λ of γ−p along γ, ∫γdz/(z−p)=λ(b)−λ(a) (The integral of dz/(z−p) along a contour is the increment of a continuous logarithm).

[L3]

For a complex contour γ and p∉γ∗ there is a continuous logarithm of γ−p along γ (Every contour missing a point admits a continuous logarithm, unique up to a constant in 2πiZ), namely a continuous λ:[a,b]→C with exp⁡(λ(t))=γ(t)−p for every t (Continuous logarithms and continuous arguments along a contour).

[L4]

ker⁡(exp⁡)=2πiZ, and exp⁡z=exp⁡w exactly when z−w∈2πiZ (ker⁡(exp⁡)=2πiZ, and exp⁡z=exp⁡w exactly when z−w∈2πiZ).

[L5]

A complex contour is closed when γ(a)=γ(b) (Rectifiable complex contours, reversal, concatenation, closedness, and orientation).

Proof

technique · direct
1.1givenL1L2L3

By [L3] fix a continuous logarithm λ of γ−p along γ; then [L1] and [L2] give 2πi n(γ,p)=λ(b)−λ(a).

1.2givenL3L5

Since γ is closed, γ(b)=γ(a) by [L5], so exp⁡(λ(b))=γ(b)−p=γ(a)−p=exp⁡(λ(a)).

2.1step 1.1step 1.2L4

By [L4] the equality of exponentials in step 1.2 gives λ(b)−λ(a)∈2πiZ, so step 1.1 makes 2πi n(γ,p) an element of 2πiZ.

3.1step 2.1L2L3L6∎

Dividing by 2πi in step 2.1 puts n(γ,p) in Z by [L6]. The argument used only the rectifiability of γ, through [L2] and [L3], and never a derivative of γ.

Depends on

Used by

Dependency tree · two levels

43 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