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 is the increment of a continuous argument divided by
Statement
Let be a closed complex contour, let , let be a continuous logarithm of along and let be the associated continuous argument (Continuous logarithms and continuous arguments along a contour). Then
In particular is an integer multiple of , and it is the same for every continuous argument of along .
Facts & Assumptions
Given: A closed complex contour , a point , a continuous logarithm of along , and .
For a closed complex contour and off its trace, (The winding number of a closed contour is an integer), where (The winding number of a closed contour about a point off its trace).
A continuous logarithm of along is a continuous with for every , its continuous argument is , and any two continuous logarithms differ by a constant in (Continuous logarithms and continuous arguments along a contour, Every contour missing a point admits a continuous logarithm, unique up to a constant in ).
For real , (, , and ).
For a complex contour , and a continuous logarithm of along , (The integral of along a contour is the increment of a continuous logarithm).
For , is the unique real with (The natural logarithm as the inverse of the exponential function).
For with real, and (Real and imaginary parts, complex conjugation, and modulus).
A complex contour is closed when (Rectifiable complex contours, reversal, concatenation, closedness, and orientation).
The integers form a commutative ring (The integers form a commutative ring).
Proof
Writing as in [L6], the identity of [L2] and the modulus formula [L3] give , so by [L5].
Since is closed, by [L7], so .
Steps 1.1 and 1.2 give , hence by [L6].
By [L1] and [L4], , which step 2.1 rewrites as ; dividing by gives .
Since is an integer by [L1] and [L8], step 3.1 makes an integer multiple of ; and replacing by another continuous logarithm changes it by a constant of by [L2], which cancels in the increment, so the value is the same for every continuous argument.
Depends on
- The winding number of a closed contour is an integer
- The winding number of a closed contour about a point off its trace
- Continuous logarithms and continuous arguments along a contour
- Every contour missing a point admits a continuous logarithm, unique up to a constant in $2\pi i\mathbb{Z}$
- $\exp(x+iy)=e^x(\cos y+i\sin y)$, $|\exp(x+iy)|=e^x$, and $e^{i\pi}+1=0$
- The integral of $dz/(z-p)$ along a contour is the increment of a continuous logarithm
- The natural logarithm as the inverse of the exponential function
- Real and imaginary parts, complex conjugation, and modulus
- Rectifiable complex contours, reversal, concatenation, closedness, and orientation
- The integers as equivalence classes of pairs of naturals
- The integers form a commutative ring
Used by
Dependency tree · two levels
62 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
- M. Weber, Complex Analysis (Indiana University), Ch. 4 §4.1 (standard reference, not scraped)