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 constant on each connected component of the complement of the trace
Statement
Let be a closed complex contour with trace and length . Then is open, and the index function satisfies the quantitative estimate
In particular is continuous on ; it is constant on every connected component of that set; and since those components are open, it is locally constant.
Facts & Assumptions
Given: A closed complex contour ; the plane carries the Euclidean metric of as the Euclidean plane and as a normed real algebra: what the identification preserves.
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).
For a complex contour and , the distance exists and is positive (A contour missing a point subdivides into arcs lying in discs that miss it).
If on the trace of a rectifiable contour , with , then (ML estimate: a contour integral is bounded by a supremum bound times path length).
For continuous on the trace of a rectifiable contour and , (Complex line integrals are linear in the integrand).
The connected component is the union of all connected subsets containing , hence the largest connected subset containing (Connected components, quasicomponents, and totally disconnected spaces).
Every connected component of an open subset is open in and polygonally connected (Every connected component of an open subset of is open and polygonally connected).
The continuous image of a connected subset is connected (A continuous image of a connected space is connected, and connectedness is a topological property), and a connected subset of is order-convex (The connected subspaces of with its usual topology are exactly the order-convex subsets, the published characterisation transported by the identification of the two descriptions of "open in ").
A compact subset of a metric space is closed and bounded (A compact subset of a metric space is closed and bounded); the continuous image of a compact subset is compact (The image of a compact metric space under a continuous map is compact, and so is the image of any compact subset); and a closed bounded interval is compact (Heine-Borel in : with the Euclidean metric a subset of is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line).
A set is closed exactly when its complement is open (The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement), and (Open ball, closed ball and sphere in a metric space).
The integers form an ordered commutative ring, and their canonical image in is discrete; hence if then lies strictly between them and is not an integer (The integers form a commutative ring, The integers form a totally ordered ring, Integer part: for every real there is exactly one integer with ).
Proof
The trace is the continuous image of a compact interval, hence compact and closed by [L9], so its complement is open by [L10].
Fix and put , which is positive by [L3]; let satisfy . For one has and, by [L11], , so as well.
For , elementary algebra gives , whose modulus is at most by step 1.2 and [L11].
By [L1] and [L5] the difference is , and [L4] with the bound of step 2.1 makes its modulus at most .
Step 3.1 shows is continuous at every , since the bound tends to with .
Let be a connected component of . By [L2] the function is integer-valued, and by step 4.1 it is continuous, so by [L6] and [L8] its image on is an order-convex subset of contained in ; by [L12] such a set has at most one element, so is constant on . By [L7] applied to the open set of step 1.1, is open, so the index is locally constant on .
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
- A contour missing a point subdivides into arcs lying in discs that miss it
- ML estimate: a contour integral is bounded by a supremum bound times path length
- Complex line integrals are linear in the integrand
- Connected components, quasicomponents, and totally disconnected spaces
- Every connected component of an open subset of $\mathbb{R}^n$ is open and polygonally connected
- A continuous image of a connected space is connected, and connectedness is a topological property
- The connected subspaces of $\mathbb{R}$ with its usual topology are exactly the order-convex subsets, the published characterisation transported by the identification of the two descriptions of "open in $\mathbb{R}$"
- A compact subset of a metric space is closed and bounded
- The image of a compact metric space under a continuous map is compact, and so is the image of any compact subset
- Heine-Borel in $\mathbb{R}^n$: with the Euclidean metric a subset of $\mathbb{R}^n$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line
- The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement
- Open ball, closed ball and sphere 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
- The integers form a totally ordered ring
- Integer part: for every real $x$ there is exactly one integer $m$ with $m \le x < m + 1$
- $\mathbb C=\mathbb R[x]/(x^2+1)$ as the Euclidean plane and as a normed real algebra: what the identification preserves
Used by
Dependency tree · two levels
127 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, Property (ii) (standard reference, not scraped)
- J. Lebl, Complex Analysis, Ch. 4 §4.1 (standard reference, not scraped)