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 argument-principle integral is the winding number of the image cycle
Statement
Let be a closed complex contour, let be meromorphic on a neighbourhood of , and suppose for every . Then is a closed complex contour with , and
Equivalently, if is any continuous argument of , then
If is also admissible and null-homologous in a larger open set on which is meromorphic, then the same integer equals by The argument principle for an admissible null-homologous cycle.
Facts & Assumptions
Given: A closed complex contour , a meromorphic function on a neighbourhood of , and on .
The winding number of a closed contour about a point off its trace is (The winding number of a closed contour about a point off its trace).
The winding number is also the normalized increment of any continuous argument (The winding number is the increment of a continuous argument divided by ).
A contour missing the origin admits a continuous logarithm, unique up to a constant in (Every contour missing a point admits a continuous logarithm, unique up to a constant in ).
A holomorphic nonvanishing function on a disc has a holomorphic logarithm, and that logarithm has derivative (A nonvanishing holomorphic function on a disc has a holomorphic logarithm, A holomorphic logarithm is a primitive of the logarithmic derivative).
Contour integrals add under concatenation, and a primitive computes the integral by endpoint increments (Complex line integrals change sign under reversal and add under concatenation, The line integral of a continuous function admitting a primitive is that primitive's endpoint increment along every rectifiable path).
Proof
Since is continuous on the compact set and never vanishes there, is a closed complex contour whose trace misses . By [L3], choose a continuous logarithm of . Cover by finitely many open discs on which has no zeros, and then subdivide into consecutive subcontours whose traces lie in those discs.
Fix . On , [L4] gives a holomorphic logarithm of , with . Along the trace of , both and are continuous logarithms of , so [L3] makes their difference constant. Therefore where the last equality is [L5] applied to the primitive .
Summing the equalities of step 2.1 over the subdivision and using the additivity from [L5] gives Now [L1] and [L2] applied to the contour identify the same increment with both and , so the two displayed formulas follow.
Depends on
- The argument principle for an admissible null-homologous cycle
- 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$
- Every contour missing a point admits a continuous logarithm, unique up to a constant in $2\pi i\mathbb{Z}$
- A nonvanishing holomorphic function on a disc has a holomorphic logarithm
- A holomorphic logarithm is a primitive of the logarithmic derivative
- Complex line integrals change sign under reversal and add under concatenation
- The line integral of a continuous function admitting a primitive is that primitive's endpoint increment along every rectifiable path
Used by
Dependency tree · two levels
64 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
- R. W. Howell and J. H. Mathews, Complex Analysis, §8.7, Theorem 8.7.9 (standard reference, not scraped)
- J. Lebl, Guide to Cultivating Complex Analysis, §5.4 (standard reference, not scraped)