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.
For loops in C times, the winding number about 0 equals the circle degree
Statement
Let be a closed rectifiable loop with , and define
Under the standard homeomorphism from to the unit circle, the loop determines a based loop in at , and
Equivalently, the winding number of about is exactly the integer that classifies the normalized circle loop of .
Facts & Assumptions
Given: A closed rectifiable loop with .
For a closed complex contour in and a continuous argument of about , one has (The winding number is the increment of a continuous argument divided by , The winding number of a closed contour about a point off its trace).
The map is a homeomorphism from to the unit circle and sends to ( is a homeomorphism from to the unit circle).
The degree of a based loop in is the endpoint of its unique lift to beginning at (The degree of a based circle loop).
The unit circle has fundamental group under the standard trigonometric normalization (The trigonometric loops give ).
Proof
Because for every , the normalized map is a continuous loop in the unit circle based at . Using the homeomorphism of [L2], regard the same loop as a based loop at . Let be its lift with , and define .
By the definition of in [L2], the lift from step 1.1 supplies a continuous argument. [step 1.1, L1, L2, algebra] Hence so is a continuous argument of about . Therefore [L1] gives
Since is exactly the degree of by [L3], step 2.1 shows , which is the asserted degree of the normalized circle loop of . Fact [L4] records that this is the same integer that classifies the loop class in the usual convention.
Depends on
- The winding number of a closed contour about a point off its trace
- The winding number is the increment of a continuous argument divided by $2\pi$
- The degree of a based circle loop
- $[t]\mapsto(\cos 2\pi t,\sin 2\pi t)$ is a homeomorphism from $\mathbb R/\mathbb Z$ to the unit circle
- The trigonometric loops give $\pi_1(\{(x,y):x^2+y^2=1\},(1,0))\cong\mathbb Z$
Used by
Dependency tree · two levels
44 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)
- J. Lebl, Guide to Cultivating Complex Analysis, Ch. 4, §4.1 (standard reference, not scraped)