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 be a closed complex contour and let with . Then
No differentiability of is used: the contour is only assumed rectifiable.
Facts & Assumptions
Given: A closed complex contour and a point .
For a closed complex contour and , (The winding number of a closed contour about a point off its trace).
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).
For a complex contour and there is a continuous logarithm of along (Every contour missing a point admits a continuous logarithm, unique up to a constant in ), namely a continuous with for every (Continuous logarithms and continuous arguments along a contour).
, and exactly when (, and exactly when ).
A complex contour is closed when (Rectifiable complex contours, reversal, concatenation, closedness, and orientation).
is the ring of integers (The integers as equivalence classes of pairs of naturals).
Proof
By [L3] fix a continuous logarithm of along ; then [L1] and [L2] give .
Since is closed, by [L5], so .
By [L4] the equality of exponentials in step 1.2 gives , so step 1.1 makes an element of .
Dividing by in step 2.1 puts in by [L6]. The argument used only the rectifiability of , through [L2] and [L3], and never a derivative of .
Depends on
The winding number of a closed contour about a point off its trace
The integral of along a contour is the increment of a continuous logarithm
Every contour missing a point admits a continuous logarithm, unique up to a constant in
Continuous logarithms and continuous arguments along a contour
, and exactly when
Rectifiable complex contours, reversal, concatenation, closedness, and orientation
The integers as equivalence classes of pairs of naturals