CorollaryStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-26

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 index of a cycle is locally constant off its trace and vanishes far from it

Statement

Let $Γ = \sum_{k < r} m_{k} γ_{k}$ be a complex chain which is a cycle, and put $M (Γ) = \sum_{k < r, m_{k} \neq 0} ∣ m_{k} ∣ L (γ_{k})$ . Then the trace $Γ^{*}$ is compact, $C ∖ Γ^{*}$ is open, and:

for $p_{0} \notin Γ^{*}$ with $d = \inf {∣ w - p_{0} ∣ : w \in Γ^{*}}$ and $∣ p - p_{0} ∣ < d / 2$ , $∣ n (Γ, p) - n (Γ, p_{0}) ∣ \leq \frac{M (Γ) ∣ p - p_{0} ∣}{π d^{2}},$ so $n (Γ, \cdot)$ is continuous on $C ∖ Γ^{*}$ ;
$n (Γ, \cdot)$ is constant on every connected component of $C ∖ Γ^{*}$ , and each such component is open, so the index is locally constant;
there is $R > 0$ with $n (Γ, p) = 0$ for every $p$ with $∣ p ∣ > R$ .

Consequently $Ω_{0} : = {p \in C ∖ Γ^{*} : n (Γ, p) = 0}$ is open and contains ${p : ∣ p ∣ > R}$ .

If $Γ^{*} = \emptyset$ then $d$ is the infimum of the empty set and clause 1 is not asserted; in that case $n (Γ, p) = 0$ for every $p \in C$ and clauses 2 and 3 hold with $Ω_{0} = C$ .

Facts & Assumptions

Given: A cycle $Γ = \sum_{k < r} m_{k} γ_{k}$ ; the plane carries the Euclidean metric of $C = R [x] / (x^{2} + 1)$ as the Euclidean plane and as a normed real algebra: what the identification preserves.

[L1]

The index of a cycle about a point off its trace is an integer (The index of a cycle about a point off its trace is an integer).

[L2]

A complex chain is a finite list of pairs $(m_{k}, γ_{k})$ and its trace is the union of the $γ_{k}^{*}$ with $m_{k} \neq 0$ (Complex chains, their traces, and cycles).

[L3]

$\int_{Γ} f d z = \sum_{k < r, m_{k} \neq 0} m_{k} \int_{γ_{k}} f d z$ , and $n (Γ, p) = (2 π i)^{- 1} \int_{Γ} d z / (z - p)$ for $p \notin Γ^{*}$ (Integration over a complex chain and the index of a chain).

[L4]

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).

[L5]

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).

[L6]

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); a finite union of compact subsets is compact (A closed subspace of a compact space is compact, and a finite union of compact subspaces is compact); a closed bounded interval is compact (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).

[L7]

The connected component $C (x)$ is the union of all connected subsets containing $x$ (Connected components, quasicomponents, and totally disconnected spaces), and every component of an open subset of $R^{n}$ is open and polygonally connected (Every connected component of an open subset of $R^{n}$ is open and polygonally connected).

[L8]

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 $R$ is order-convex (The connected subspaces of $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 $R$ ").

[L9]

A set is closed exactly when its complement is open, and a set is open exactly when each of its points admits a ball inside it (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); a subset is bounded when it is empty or lies inside some ball (Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space).

[L10]

A nonempty subset of $R$ bounded below has a greatest lower bound (Every nonempty set bounded below has an infimum, Greatest lower bound (infimum)).

[L11]

$∣ z w ∣ = ∣ z ∣ ∣ w ∣$ and $∣ z + w ∣ \leq ∣ z ∣ + ∣ w ∣$ for complex $z, w$ (Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive).

[L12]

Finite sums in the additive commutative monoid of $C$ are additive, and complex-field distributivity permits scaling term by term (A finite sum in a commutative monoid indexed by an arbitrary finite set, $C = R [x] / (x^{2} + 1)$ is a field, every element is uniquely $a + b i$ , and every nonzero element has inverse $(a - b i) / (a^{2} + b^{2})$ ).

[L13]

The integers form an ordered commutative ring and are discrete in $R$ ; in particular the only integer of modulus below $1$ is $0$ , and if $m < n$ then $m + \frac{1}{2}$ 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 $x$ there is exactly one integer $m$ with $m \leq x < m + 1$ ).

Proof

technique · direct

1.1

Each $γ_{k}^{*}$ is the continuous image of a compact interval, hence compact by [L6], so the trace $Γ^{*}$ of [L2] is a finite union of compact sets and is compact by [L6], closed and bounded by [L6], and its complement is open by [L9].

givenL2L6L9

2.1

Suppose $Γ^{*} \neq \emptyset$ , fix $p_{0} \notin Γ^{*}$ and put $d = \inf {∣ w - p_{0} ∣ : w \in Γ^{*}}$ , which exists by [L10] and is positive because the complement of the closed set $Γ^{*}$ is open, so some ball $B (p_{0}, ε)$ misses $Γ^{*}$ and $d \geq ε$ by [L9]. For $∣ p - p_{0} ∣ < d / 2$ and $z \in Γ^{*}$ one has $∣ z - p_{0} ∣ \geq d$ and $∣ z - p ∣ > d / 2 > 0$ by [L11], so $p \notin Γ^{*}$ and $∣ \frac{1}{z - p} - \frac{1}{z - p_{0}} ∣ = ∣ \frac{p - p_{0}}{(z - p) (z - p_{0})} ∣ \leq 2 ∣ p - p_{0} ∣ / d^{2}$ .

step 1.1L9L10L11algebra

2.2

Let $R_{0} > 0$ satisfy $Γ^{*} \subseteq {z : ∣ z ∣ \leq R_{0}}$ , available from the boundedness in step 1.1 and [L9]. For $∣ p ∣ > R_{0}$ and $z \in Γ^{*}$ , [L11] gives $∣ z - p ∣ \geq ∣ p ∣ - R_{0} > 0$ , so [L3], [L4] and [L12] give $∣ n (Γ, p) ∣ \leq M (Γ) / (2 π (∣ p ∣ - R_{0}))$ .

step 1.1L3L4L9L11L12

3.1

For $k$ with $m_{k} \neq 0$ the trace $γ_{k}^{*}$ lies in $Γ^{*}$ , so the bound of step 2.1 holds on it and [L4] gives $∣ \int_{γ_{k}} (\frac{1}{z - p} - \frac{1}{z - p_{0}}) d z ∣ \leq 2 ∣ p - p_{0} ∣ L (γ_{k}) / d^{2}$ ; combining the terms with [L3], [L5], [L11] and [L12] yields $∣ n (Γ, p) - n (Γ, p_{0}) ∣ \leq M (Γ) ∣ p - p_{0} ∣ / (π d^{2})$ , which is clause 1 and makes $n (Γ, \cdot)$ continuous at $p_{0}$ .

step 2.1L3L4L5L11L12

3.2

Take $R = R_{0} + M (Γ) / (2 π) + 1$ . For $∣ p ∣ > R$ step 2.2 gives $∣ n (Γ, p) ∣ < 1$ , and $n (Γ, p)$ is an integer by [L1], so it is $0$ by [L13]; this is clause 3.

step 2.2L1L13

4.1

Let $C$ be a connected component of $C ∖ Γ^{*}$ . By [L7], applied to the open set of step 1.1, the component $C$ is open and polygonally connected, hence connected; by [L1] the index is integer-valued and by step 3.1 it is continuous, so [L8] makes its image on $C$ a connected subset of $R$ . That image lies in $Z$ , so [L13] forces it to be a single point. This is clause 2.

step 1.1step 3.1L1L7L8L13

5.1

By step 4.1 the set $Ω_{0}$ is a union of components of the open set $C ∖ Γ^{*}$ , each open by [L7], hence open; and it contains ${p : ∣ p ∣ > R}$ by step 3.2. If $Γ^{*} = \emptyset$ then every $m_{k}$ is zero or $r = 0$ , so $\int_{Γ} f d z = 0$ for every $f$ by [L3] and $n (Γ, p) = 0$ for every $p \in C$ , giving $Ω_{0} = C$ .

step 3.2step 4.1L3L7∎

Depends on

Used by

Dependency tree · two levels

147 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 §4.4 (standard reference, not scraped)