LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6.1-sol)

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 locally constant by an integral estimate

Statement

Let $Γ$ be a closed rectifiable contour of length $L$ and let $p_{0}$ lie off its trace. If $d > 0$ satisfies $∣ z - p_{0} ∣ \geq d$ for all $z \in Γ^{*}$ and $∣ p - p_{0} ∣ < d / 2$ , then $∣ n (Γ, p) - n (Γ, p_{0}) ∣ \leq L ∣ p - p_{0} ∣ / (π d^{2})$ . In particular the winding number is locally constant on the complement of the trace.

Facts & Assumptions

Given: A closed rectifiable contour $Γ$ of length $L$ , a point $p_{0}$ off its trace, and a number $d > 0$ with $∣ z - p_{0} ∣ \geq d$ for all $z \in Γ^{*}$ .

[F1]

For a closed complex contour $γ$ and a point $p$ off its trace, $n (γ, p) = \frac{1}{2 π i} \int_{γ} \frac{d z}{z - p}$ . (The winding number of a closed contour about a point off its trace).

[F2]

For continuous $f, g$ on the trace of a rectifiable contour $γ$ and $α, β \in C$ , $\int_{γ} (α f + β g) d z = α \int_{γ} f d z + β \int_{γ} g d z$ . (Complex line integrals are linear in the integrand).

[F3]

If $∣ f (z) ∣ \leq M$ on the trace of a rectifiable contour $γ$ with $M \geq 0$ , then $∣ \int_{γ} f (z) d z ∣ \leq M L (γ)$ . (ML estimate: a contour integral is bounded by a supremum bound times path length).

[F4]

A closed box in $R^{n}$ is a compact subset of Euclidean space. (Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $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).

[F5]

For a closed complex contour $γ$ and a point $p$ off its trace, $n (γ, p) \in Z$ . (The winding number of a closed contour is an integer).

Proof

technique · direct

1.1givenF1

Let $p$ satisfy $∣ p - p_{0} ∣ < d / 2$ ; then $∣ z - p ∣ \geq ∣ z - p_{0} ∣ - ∣ p - p_{0} ∣ > d - d / 2 = d / 2 > 0$ for every $z \in Γ^{*}$ , so $p$ also lies off the trace and both winding numbers are defined by the contour integral of the corresponding $1 / (z - p)$ .

2.1F1F2step 1.1

Subtracting the two integrands gives $\frac{1}{z - p} - \frac{1}{z - p_{0}} = \frac{p - p_{0}}{(z - p) (z - p_{0})}$ for $z \in Γ^{*}$ , so by linearity of complex line integrals $n (Γ, p) - n (Γ, p_{0}) = \frac{1}{2 π i} \int_{Γ} \frac{p - p_{0}}{(z - p) (z - p_{0})} d z$ .

2.2F3step 1.1

On the trace $∣ z - p ∣ \geq d / 2$ and $∣ z - p_{0} ∣ \geq d$ , so the integrand has modulus at most $2 ∣ p - p_{0} ∣ / d^{2}$ ; the ML estimate with the length $L$ of $Γ$ and the factor $(2 π i)^{- 1}$ give $∣ n (Γ, p) - n (Γ, p_{0}) ∣ \leq L ∣ p - p_{0} ∣ / (π d^{2})$ , the displayed estimate.

3.1F4step 2.2

For the local-constancy assertion fix $p_{0}$ off the trace; if $L = 0$ the estimate of step 2.2 bounds the defining integral by $0$ for every point off the trace, so the winding number vanishes near $p_{0}$ ; if $L > 0$ , then for each parameter $t$ continuity of the rectifiable contour supplies a relative interval $J$ containing $t$ on which $∣ Γ (s) - p_{0} ∣ > ∣ Γ (t) - p_{0} ∣ / 2$ , the family of all such pairs $(t, J)$ covers the compact parameter interval, so finitely many cover it by [F4], and the minimum of the finitely many positive numbers $∣ Γ (t_{i}) - p_{0} ∣ / 2$ is a $d > 0$ with $∣ z - p_{0} ∣ \geq d$ on $Γ^{*}$ .

4.1F5step 3.1∎

With that $d$ the estimate of step 2.2 gives $∣ n (Γ, p) - n (Γ, p_{0}) ∣ \leq L ∣ p - p_{0} ∣ / (π d^{2})$ , which is less than $1$ whenever $∣ p - p_{0} ∣ < \min (d / 2, π d^{2} / L)$ ; the difference of the two winding numbers is an integer by [F5], so it vanishes for every $p$ in that relative neighbourhood of $p_{0}$ , and since $p_{0}$ was an arbitrary point off the trace the winding number is locally constant on the complement of the trace; no general Jordan theorem or choice principle is used.

Depends on

Used by

A finitely cornered regular plane curve separates without choice Lemma

Dependency tree · two levels

48 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-2.3 (the index of a closed curve, its local constancy, and the Cauchy integral formula) (standard reference, not scraped)
J. Lebl, Complex Analysis (open text), Ch. 4 §4.1 (the index of a closed curve) (standard reference, not scraped)