Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

A circle traversed k times has winding number k inside and 0 outside

Statement

Let aC, let r>0, let kZ and put

γk(t)=a+rexp(ikt),t[0,2π].

Then γk is a closed complex contour and

n(γk,z)=kfor za<r,n(γk,z)=0for za>r.

For k0 the trace of γk is the circle {z:za=r}. For k=0 the contour is the constant path at a+r and its trace is {a+r}; the two displayed formulas still hold, both values being 0, and both regions still lie off the trace.

Facts & Assumptions

Given: A point aC, a real r>0 and an integer k.

[L1]

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

[L2]

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).

[L3]

The index is constant on every connected component of the complement of the trace (The winding number is constant on each connected component of the complement of the trace).

[L4]

The complement of the trace of a closed complex contour has exactly one unbounded connected component, and the index vanishes there (The winding number vanishes on the unbounded component of the complement of the trace); for a compact K the complement CK has exactly one unbounded component and every other component is bounded (The complement of a compact plane set has exactly one unbounded connected component).

[L5]

For cC and R>0 the set {z:zc>R} is path-connected and connected (The exterior of a closed disc in the plane is path-connected).

[L6]

For a complex contour γ:[a,b]C, a point pγ and a continuous logarithm λ of γp along γ, γdz/(zp)=λ(b)λ(a) (The integral of dz/(zp) along a contour is the increment of a continuous logarithm); such a λ is a continuous map with exp(λ(t))=γ(t)p throughout (Continuous logarithms and continuous arguments along a contour).

[L7]

For a positively oriented circle σ(t)=a+rexp(it) with r>0, (2πi)1σdz/(za)=1 (The normalized integral around a positively oriented circle centred at a is 1).

[L8]

exp(z+w)=expzexpw for all complex z,w, and exp(x+0i)=ex for real x (exp(z+w)=expzexpw, and the complex exponential extends the real exponential); for real x,y, exp(x+iy)=ex(cosy+isiny) and exp(x+iy)=ex (exp(x+iy)=ex(cosy+isiny), exp(x+iy)=ex, and eiπ+1=0).

[L10]

t(cost,sint) is a bijection from [0,2π) onto the unit circle S1 (t(cost,sint) is a bijection from [0,2π) onto the real unit circle), and cos and sin have fundamental period 2π (The zero sets of sine and cosine and the least positive common period 2 pi).

[L11]

cos and sin are differentiable on R with cos=sin and sin=cos (The derivatives of sine and cosine are cosine and minus sine).

[L12]

A continuous path that is differentiable with a continuous derivative on each piece of a partition is rectifiable (A continuous piecewise-C1 path is rectifiable and its length is the sum of the speed integrals over its pieces).

[L13]

For x>0, logx is the unique real y with expy=x (The natural logarithm as the inverse of the exponential function).

[L14]

B(x,ρ)={y:d(x,y)<ρ} (Open ball, closed ball and sphere in a metric space); a set is convex when it contains the segment between any two of its points (A convex subset of Rm contains every line segment between two of its points); a subset joined by paths inside it is path-connected (Paths, path-connected spaces and path components) and hence connected (Every path-connected space is connected, and every path component lies inside a component).

[L15]

Distinct components are disjoint and every connected subset containing a point lies inside that point's component (The components of a space are its maximal connected subsets, they partition it, and each of them is closed, Connected components, quasicomponents, and totally disconnected spaces).

[L16]

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).

[L17]

zw=zw and z+wz+w (Conjugation is an involutive real-field automorphism, zz=z2, and modulus is definite, multiplicative, and subadditive).

[L18]

The integers form a commutative ring (The integers form a commutative ring).

Proof

technique · direct
1.1

By [L8] one has γk(t)=a+rcos(kt)+irsin(kt), which by [L11] is differentiable in t with the continuous derivative krsin(kt)+ikrcos(kt), so γk is rectifiable by [L12]; and γk(2π)=a+rexp(2πik)=a+r=γk(0) by [L9], so γk is a closed complex contour.

givenL8L9L11L12
1.2

Since γk(t)a=rexp(ikt)=r>0 by [L8] and [L17], the centre a lies off the trace, and λ(t)=logr+ikt is a continuous map on [0,2π] with exp(λ(t))=elogrexp(ikt)=rexp(ikt)=γk(t)a by [L8] and [L13]; so λ is a continuous logarithm of γka along γk in the sense of [L6].

givenL6L8L13L17
1.3

The trace of γk is {a+rexp(ikt):0t2π}. If k=0 this is {a+r}. If k0 then {kt:0t2π} is a closed interval of length 2πk2π, so by the periodicity and surjectivity in [L10] the values exp(iks) run over the whole unit circle, and the trace is {z:za=r} by [L8] and [L17]. In both cases the trace is contained in {z:za=r}.

givenL8L10L17
2.1

By [L6] and step 1.2, γkdz/(za)=λ(2π)λ(0)=2πik, so n(γk,a)=k by [L1]; for k=1 this is the published normalisation [L7], and by [L2] and [L18] the value is an integer, as it must be.

step 1.1step 1.2L1L2L6L7L18
2.2

The disc D=B(a,r) is convex by [L14] and [L17], hence path-connected along segments and therefore connected; step 1.3 puts the trace in {z:za=r}, which is disjoint from D, so DCγk and aD.

step 1.3L14L17
2.3

The set E={z:za>r} is connected by [L5] and is disjoint from the trace by step 1.3; it is unbounded by [L16] and [L17], so by [L15] it lies in a single component of Cγk, and that component is unbounded, hence is the unique unbounded one of [L4].

step 1.3L4L5L15L16L17
3.1

By [L3] the index is constant on the component of Cγk containing D, and D is a connected subset of that complement containing a, so by [L15] it lies in one component; hence n(γk,z)=n(γk,a)=k for every zD, that is for za<r.

step 2.1step 2.2L3L15
4.1

By [L4] the index vanishes on that unique unbounded component, so n(γk,z)=0 for every zE by step 2.3, while step 3.1 gives the value k on za<r; when k=0 both regions still lie off the single-point trace of step 1.3 and both values are 0.

step 3.1step 2.3L4

Depends on

Used by

Dependency tree · two levels

128 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