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.
Reversal negates and concatenation adds winding numbers
Statement
Reversal. Let be a closed complex contour and let . Then the reversal is a closed complex contour with the same trace, and
Concatenation. Let be complex contours with . Then is a complex contour with trace , and for every
If moreover and are themselves closed, then is closed and
The hypothesis is what makes the concatenation a contour, and closedness of is what makes its index defined; the integral identity needs neither nor to be closed.
Facts & Assumptions
Given: Closed complex contours where an index is asserted, composable complex contours where a concatenation is asserted, and a point off the traces involved.
For a closed complex contour and , (The winding number of a closed contour about a point off its trace).
For a rectifiable contour , ; for composable rectifiable contours , (Complex line integrals change sign under reversal and add under concatenation).
A complex contour is a rectifiable path ; it is closed when ; its reversal is ; and for with the concatenation is for and for (Rectifiable complex contours, reversal, concatenation, closedness, and orientation, Reversal, concatenation, closed paths, and oriented piecewise-C1 reparametrizations).
Arc length is unchanged by a monotone reparametrization (Arc length is invariant under every continuous surjective monotone reparametrization, including pauses and reversal).
Arc length is additive across a split of the parameter interval, and a path is rectifiable exactly when both restrictions are (Arc length is additive across every subdivision point and decreases under restriction).
For a rectifiable contour and a continuous integrand on its trace, the complex line integral exists (Continuous integrands have complex and absolute line integrals along every rectifiable path).
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).
Proof
The map is a decreasing continuous bijection of onto itself, so by [L3] and [L4] the reversal is a path of the same length as , hence rectifiable, and its trace is ; it is closed because by [L3].
By [L3] the concatenation is continuous on , its restrictions to and are monotone reparametrizations of and , so both are rectifiable by [L4] and is rectifiable by [L5]; its trace is by the two-piece formula.
If and are closed then by [L3], so is closed.
With the function is continuous on , so all the integrals below exist by [L6]; applying the reversal identity of [L2] to it and dividing by gives through [L1].
With the function is continuous on that union, so the concatenation identity of [L2] applies to it and gives the displayed additive formula, all three integrals existing by [L6].
If and are closed, step 1.3 makes closed, so [L1] turns step 2.2 into ; all three values are integers by [L7], consistently with the identity.
Depends on
- The winding number of a closed contour about a point off its trace
- Complex line integrals change sign under reversal and add under concatenation
- Rectifiable complex contours, reversal, concatenation, closedness, and orientation
- Reversal, concatenation, closed paths, and oriented piecewise-C1 reparametrizations
- Arc length is invariant under every continuous surjective monotone reparametrization, including pauses and reversal
- Arc length is additive across every subdivision point and decreases under restriction
- Continuous integrands have complex and absolute line integrals along every rectifiable path
- The winding number of a closed contour is an integer
Used by
Dependency tree · two levels
30 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
- L. V. Ahlfors, Complex Analysis, 3rd ed., Ch. 4 §2.1 (standard reference, not scraped)