TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck 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 about a point off its trace is an integer

Statement

Let $Γ = \sum_{k < r} m_{k} γ_{k}$ be a complex chain which is a cycle, that is $\partial Γ$ vanishes identically (Complex chains, their traces, and cycles), and let $p \in C$ with $p \notin Γ^{*}$ . Then

$n (Γ, p) \in Z .$

The individual contours $γ_{k}$ need not be closed; what is used is that the endpoint counts cancel. The empty cycle gives $n (Γ, p) = 0$ .

Facts & Assumptions

Given: A complex chain $Γ = \sum_{k < r} m_{k} γ_{k}$ with $γ_{k} : [a_{k}, b_{k}] \to C$ , whose boundary function vanishes identically, and a point $p \notin Γ^{*}$ .

[L1]

A complex chain is a finite list of pairs $(m_{k}, γ_{k})$ , its trace is the union of the $γ_{k}^{*}$ with $m_{k} \neq 0$ , its boundary is $\partial Γ (q) = \sum {m_{k} : γ_{k} (b_{k}) = q} - \sum {m_{k} : γ_{k} (a_{k}) = q}$ , and it is a cycle when that function vanishes identically (Complex chains, their traces, and cycles).

[L2]

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

[L3]

For a complex contour $γ : [a, b] \to C$ , a point $p \notin γ^{*}$ and a continuous logarithm $λ$ of $γ - p$ along $γ$ , $\int_{γ} d z / (z - p) = λ (b) - λ (a)$ (The integral of $d z / (z - p)$ along a contour is the increment of a continuous logarithm).

[L4]

For a complex contour $γ$ and $p \notin γ^{*}$ there is a continuous logarithm of $γ - p$ along $γ$ (Every contour missing a point admits a continuous logarithm, unique up to a constant in $2 π i Z$ ), a continuous $λ$ with $\exp (λ (t)) = γ (t) - p$ throughout (Continuous logarithms and continuous arguments along a contour).

[L5]

$\ker (\exp) = 2 π i Z$ , and $\exp z = \exp w$ exactly when $z - w \in 2 π i Z$ ( $\ker (\exp) = 2 π i Z$ , and $\exp z = \exp w$ exactly when $z - w \in 2 π i Z$ ).

[L6]

The complex exponential maps $C$ onto $C ∖ {0}$ (The complex exponential maps $C$ onto $C ∖ {0}$ ).

[L7]

Finite sums in the additive commutative group of $C$ are additive and telescope, 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})$ ).

[L8]

For disjoint finite index sets $S, T$ , $\sum_{u \in S \cup T} a_{u} = \sum_{s \in S} a_{s} + \sum_{t \in T} a_{t}$ (Finite commutative-monoid sums are invariant under bijective reindexing, split over disjoint unions, and satisfy the finite Fubini rule); sums over finite index sets are well posed and the empty sum is $0$ (A finite sum in a commutative monoid indexed by an arbitrary finite set, The cardinality $∣ A ∣$ of a finite set).

[L9]

A natural-number-indexed finite list of nonempty sets admits a choice function, provably in ZF (Every natural-number-indexed list of nonempty sets has a choice function on its family of values).

[L10]

The integers form a commutative ring (The integers form a commutative ring).

Proof

technique · direct

1.1givenL1L8

Write $K = {k < r : m_{k} \neq 0}$ and let $Q = {γ_{k} (a_{k}) : k \in K} \cup {γ_{k} (b_{k}) : k \in K}$ , a finite subset of $Γ^{*}$ by [L1]; in particular $q - p \neq 0$ for every $q \in Q$ , since $p \notin Γ^{*}$ .

1.2givenL4L6L9

For each $k \in K$ the point $p$ lies off $γ_{k}^{*} \subseteq Γ^{*}$ , so [L4] provides a continuous logarithm $λ_{k}$ of $γ_{k} - p$ along $γ_{k}$ ; finitely many such choices are made, which is legitimate in ZF by [L9]. Likewise [L6] and [L9] provide, for each $q \in Q$ , a complex number $μ (q)$ with $\exp (μ (q)) = q - p$ .

2.1step 1.2L2L3

By [L2] and [L3], $n (Γ, p) = \frac{1}{2 π i} \sum_{k \in K} m_{k} (λ_{k} (b_{k}) - λ_{k} (a_{k}))$ .

2.2step 1.1step 1.2L5

Fix $k \in K$ . Since $\exp (λ_{k} (a_{k})) = γ_{k} (a_{k}) - p = \exp (μ (γ_{k} (a_{k})))$ and similarly at $b_{k}$ , [L5] gives integers $u_{k}, v_{k}$ with $λ_{k} (a_{k}) = μ (γ_{k} (a_{k})) + 2 π i u_{k}$ and $λ_{k} (b_{k}) = μ (γ_{k} (b_{k})) + 2 π i v_{k}$ ; hence $λ_{k} (b_{k}) - λ_{k} (a_{k}) = μ (γ_{k} (b_{k})) - μ (γ_{k} (a_{k})) + 2 π i (v_{k} - u_{k})$ .

3.1step 2.1step 2.2L7L10

Substituting step 2.2 into step 2.1 and using [L7], one gets $n (Γ, p) = \frac{S}{2 π i} + \sum_{k \in K} m_{k} (v_{k} - u_{k})$ , where $S = \sum_{k \in K} m_{k} μ (γ_{k} (b_{k})) - \sum_{k \in K} m_{k} μ (γ_{k} (a_{k}))$ . The second summand is an integer by [L10].

4.1step 1.1step 3.1L1L7L8

The index set $K$ is the disjoint union over $q \in Q$ of ${k \in K : γ_{k} (b_{k}) = q}$ , so [L8] and [L7] give $\sum_{k \in K} m_{k} μ (γ_{k} (b_{k})) = \sum_{q \in Q} μ (q) \sum {m_{k} : k \in K, γ_{k} (b_{k}) = q}$ , and likewise with $a_{k}$ in place of $b_{k}$ ; since a term with $m_{k} = 0$ contributes $0$ to the boundary sums of [L1], subtracting the two gives $S = \sum_{q \in Q} μ (q) \partial Γ (q)$ , which is $0$ because $Γ$ is a cycle.

5.1step 3.1step 4.1L8L10∎

Step 4.1 makes $S = 0$ , so step 3.1 gives $n (Γ, p) = \sum_{k \in K} m_{k} (v_{k} - u_{k})$ , an integer by [L10]. For the empty cycle $K$ is empty and the sum of step 2.1 is $0$ by [L8], giving $n (Γ, p) = 0$ .

Depends on

Used by

Dependency tree · two levels

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