TheoremStatement: 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.

Chain integration and the index are additive in the chain, and reverse with it

Statement

Let $Γ$ , $Γ_{1}$ , $Γ_{2}$ be complex chains (Complex chains, their traces, and cycles). Then:

$(Γ_{1} + Γ_{2})^{*} = Γ_{1}^{*} \cup Γ_{2}^{*}$ , $(- Γ)^{*} = Γ^{*}$ and $(Γ^{-})^{*} = Γ^{*}$ ;
$\partial (Γ_{1} + Γ_{2}) = \partial Γ_{1} + \partial Γ_{2}$ , $\partial (- Γ) = - \partial Γ$ and $\partial (Γ^{-}) = - \partial Γ$ as functions on $C$ ; consequently a sum of cycles is a cycle, and the negative and the reversal of a cycle are cycles;
for $f$ continuous on $Γ_{1}^{*} \cup Γ_{2}^{*}$ , $\int_{Γ_{1} + Γ_{2}} f d z = \int_{Γ_{1}} f d z + \int_{Γ_{2}} f d z,$ and for $f$ continuous on $Γ^{*}$ , $\int_{- Γ} f d z = - \int_{Γ} f d z, \int_{Γ^{-}} f d z = - \int_{Γ} f d z;$
for $p \notin Γ_{1}^{*} \cup Γ_{2}^{*}$ , $n (Γ_{1} + Γ_{2}, p) = n (Γ_{1}, p) + n (Γ_{2}, p)$ , and for $p \notin Γ^{*}$ , $n (- Γ, p) = - n (Γ, p) = n (Γ^{-}, p)$ ;
the empty chain is a cycle, its integral of every function is $0$ , and its index is $0$ at every point of $C$ .

Facts & Assumptions

Given: Complex chains $Γ = \sum_{k < r} m_{k} γ_{k}$ , $Γ_{1} = \sum_{k < r_{1}} m_{k}^{1} γ_{k}^{1}$ and $Γ_{2} = \sum_{k < r_{2}} m_{k}^{2} γ_{k}^{2}$ , and integrands continuous on the traces named in each clause.

[L1]

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

[L2]

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}$ ; it is a cycle when that vanishes identically; $Γ_{1} + Γ_{2}$ is list concatenation, $- Γ$ negates every coefficient, and $Γ^{-}$ reverses every contour (Complex chains, their traces, and cycles).

[L3]

For a rectifiable contour $γ$ , $\int_{γ^{-}} f d z = - \int_{γ} f d z$ (Complex line integrals change sign under reversal and add under concatenation); the reversal of a closed contour is a closed contour with the same trace and $n (γ^{-}, p) = - n (γ, p)$ (Reversal negates and concatenation adds winding numbers).

[L4]

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

[L5]

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

[L6]

For disjoint finite index sets $S, T$ and $a : S \cup T \to M$ in a commutative monoid, $\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); a sum over a finite index set is well posed and the sum over the empty set is $0$ (A finite sum in a commutative monoid indexed by an arbitrary finite set).

[L7]

For a rectifiable contour and a continuous integrand on its trace, the complex line integral exists (Continuous integrands have complex and absolute line integrals along every rectifiable path).

[L8]

The reversal of $γ : [a, b] \to C$ is $γ^{-} (t) = γ (a + b - t)$ , so its endpoints are exchanged (Rectifiable complex contours, reversal, concatenation, closedness, and orientation), and arc length is unchanged by a monotone reparametrization (Arc length is invariant under every continuous surjective monotone reparametrization, including pauses and reversal).

Proof

technique · direct

1.1

The list $Γ_{1} + Γ_{2}$ has as its terms exactly the terms of $Γ_{1}$ followed by those of $Γ_{2}$ , so the set of indices with nonzero coefficient splits as a disjoint union and [L2] gives $(Γ_{1} + Γ_{2})^{*} = Γ_{1}^{*} \cup Γ_{2}^{*}$ . Negating a coefficient does not change whether it is zero, and reversing a contour does not change its trace by [L8], so $(- Γ)^{*} = (Γ^{-})^{*} = Γ^{*}$ . This is claim 1.

givenL2L8

1.2

For each $q$ , the two defining sums of $\partial (Γ_{1} + Γ_{2}) (q)$ run over the disjoint union of the corresponding index sets for $Γ_{1}$ and $Γ_{2}$ , so [L6] splits each of them and gives $\partial (Γ_{1} + Γ_{2}) (q) = \partial Γ_{1} (q) + \partial Γ_{2} (q)$ . Replacing every $m_{k}$ by $- m_{k}$ multiplies both sums by $- 1$ by [L5], giving $\partial (- Γ) = - \partial Γ$ ; and by [L8] the reversal exchanges the roles of the two endpoint sums, giving $\partial (Γ^{-}) = - \partial Γ$ . Hence if $\partial Γ_{1}$ and $\partial Γ_{2}$ vanish identically so does $\partial (Γ_{1} + Γ_{2})$ , and likewise for $- Γ$ and $Γ^{-}$ ; this is claim 2.

givenL2L5L6L8

1.3

The empty chain has empty trace, both its boundary sums are empty and therefore $0$ by [L6], and its integral is the empty sum, which is $0$ by [L1] and [L6]; hence its index is $0$ at every $p \in C$ , all of which lie off its empty trace. This is claim 5.

L1L2L6

2.1

Let $f$ be continuous on $Γ_{1}^{*} \cup Γ_{2}^{*}$ , which by step 1.1 is the trace of $Γ_{1} + Γ_{2}$ , so all three integrals exist by [L1] and [L7]. The defining sum for $\int_{Γ_{1} + Γ_{2}} f d z$ runs over the disjoint union of the two index sets, so [L6] splits it into $\int_{Γ_{1}} f d z + \int_{Γ_{2}} f d z$ .

step 1.1L1L6L7

3.1

Let $f$ be continuous on $Γ^{*}$ . Replacing each $m_{k}$ by $- m_{k}$ multiplies each summand of [L1] by $- 1$ , so [L5] gives $\int_{- Γ} f d z = - \int_{Γ} f d z$ ; and replacing each $γ_{k}$ by $γ_{k}^{-}$ negates each $\int_{γ_{k}} f d z$ by [L3], so $\int_{Γ^{-}} f d z = - \int_{Γ} f d z$ as well. Together with step 2.1 this is claim 3.

step 1.1step 2.1L1L3L5

4.1

Applying steps 2.1 and 3.1 to $f (z) = 1 / (z - p)$ , which is continuous on the traces involved whenever $p$ lies off them, and dividing by $2 π i$ using [L4] gives claim 4: $n (Γ_{1} + Γ_{2}, p) = n (Γ_{1}, p) + n (Γ_{2}, p)$ and $n (- Γ, p) = - n (Γ, p) = n (Γ^{-}, p)$ .

step 1.3step 2.1step 3.1L1L3L4∎

Depends on

Used by

Dependency tree · two levels

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