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 times has winding number inside and outside
Statement
Let , let , let and put
Then is a closed complex contour and
For the trace of is the circle . For the contour is the constant path at and its trace is ; the two displayed formulas still hold, both values being , and both regions still lie off the trace.
Facts & Assumptions
Given: A point , a real and an integer .
For a closed complex contour and , (The winding number of a closed contour about a point off its trace).
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).
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).
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 the complement has exactly one unbounded component and every other component is bounded (The complement of a compact plane set has exactly one unbounded connected component).
For and the set is path-connected and connected (The exterior of a closed disc in the plane is path-connected).
For a complex contour , a point and a continuous logarithm of along , (The integral of along a contour is the increment of a continuous logarithm); such a is a continuous map with throughout (Continuous logarithms and continuous arguments along a contour).
For a positively oriented circle with , (The normalized integral around a positively oriented circle centred at a is 1).
for all complex , and for real (, and the complex exponential extends the real exponential); for real , and (, , and ).
is a bijection from onto the unit circle ( is a bijection from onto the real unit circle), and and have fundamental period (The zero sets of sine and cosine and the least positive common period 2 pi).
and are differentiable on with and (The derivatives of sine and cosine are cosine and minus sine).
A continuous path that is differentiable with a continuous derivative on each piece of a partition is rectifiable (A continuous piecewise- path is rectifiable and its length is the sum of the speed integrals over its pieces).
For , is the unique real with (The natural logarithm as the inverse of the exponential function).
(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 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).
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).
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).
The integers form a commutative ring (The integers form a commutative ring).
Proof
By [L8] one has , which by [L11] is differentiable in with the continuous derivative , so is rectifiable by [L12]; and by [L9], so is a closed complex contour.
Since by [L8] and [L17], the centre lies off the trace, and is a continuous map on with by [L8] and [L13]; so is a continuous logarithm of along in the sense of [L6].
The trace of is . If this is . If then is a closed interval of length , so by the periodicity and surjectivity in [L10] the values run over the whole unit circle, and the trace is by [L8] and [L17]. In both cases the trace is contained in .
By [L6] and step 1.2, , so by [L1]; for this is the published normalisation [L7], and by [L2] and [L18] the value is an integer, as it must be.
The disc is convex by [L14] and [L17], hence path-connected along segments and therefore connected; step 1.3 puts the trace in , which is disjoint from , so and .
The set 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 , and that component is unbounded, hence is the unique unbounded one of [L4].
By [L3] the index is constant on the component of containing , and is a connected subset of that complement containing , so by [L15] it lies in one component; hence for every , that is for .
By [L4] the index vanishes on that unique unbounded component, so for every by step 2.3, while step 3.1 gives the value on ; when both regions still lie off the single-point trace of step 1.3 and both values are .
Depends on
- The winding number of a closed contour about a point off its trace
- The winding number of a closed contour is an integer
- The winding number is constant on each connected component of the complement of the trace
- The winding number vanishes on the unbounded component of the complement of the trace
- The complement of a compact plane set has exactly one unbounded connected component
- The exterior of a closed disc in the plane is path-connected
- The integral of $dz/(z-p)$ along a contour is the increment of a continuous logarithm
- Continuous logarithms and continuous arguments along a contour
- The normalized integral around a positively oriented circle centred at a is 1
- $\exp(z+w)=\exp z\,\exp w$, and the complex exponential extends the real exponential
- $\exp(x+iy)=e^x(\cos y+i\sin y)$, $|\exp(x+iy)|=e^x$, and $e^{i\pi}+1=0$
- $\ker(\exp)=2\pi i\mathbb Z$, and $\exp z=\exp w$ exactly when $z-w\in2\pi i\mathbb Z$
- $t\mapsto(\cos t,\sin t)$ is a bijection from $[0,2\pi)$ onto the real unit circle
- The zero sets of sine and cosine and the least positive common period 2 pi
- The derivatives of sine and cosine are cosine and minus sine
- A continuous piecewise-$C^1$ path is rectifiable and its length is the sum of the speed integrals over its pieces
- The natural logarithm as the inverse of the exponential function
- Open ball, closed ball and sphere in a metric space
- A convex subset of $\mathbb{R}^m$ contains every line segment between two of its points
- Paths, path-connected spaces and path components
- Every path-connected space is connected, and every path component lies inside a 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
- Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space
- Conjugation is an involutive real-field automorphism, $z\overline z=|z|^2$, and modulus is definite, multiplicative, and subadditive
- The integers as equivalence classes of pairs of naturals
- The integers form a commutative ring
Used by
- A connected plane domain that is not homologically simply connected Counterexample
- A nonvanishing holomorphic function on a domain with no holomorphic logarithm Counterexample
- A disjoint two-circle cycle has indices +1 and -1 in its two components Example
- Dixon's gluing traced on the boundary cycle of an annulus Example
- Every cycle in a round annulus has one period, that of the central circle Example
- The boundary cycle of a round annulus has index 1 inside the annulus and 0 on either side Example
- The unit circle traversed three times has index 3 at every interior point Example
- The winding numbers of a keyhole contour about the origin and about an excluded point Example
- Every cycle in a connected plane domain is null-homologous in that domain False statement
- The winding number depends only on the trace of the closed contour False statement
- The winding number is the circulation of the planar vortex field divided by 2π Remark
- The iterated Cauchy integral formula on a polydisc Theorem
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
- J. Lebl, Complex Analysis, Ch. 4 §4.1 (standard reference, not scraped)