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
, , and
The integral of 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