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 integral of a continuous derivative over a cycle is zero

Statement

Let $Γ = \sum_{k < r} m_{k} γ_{k}$ be a complex chain which is a cycle, let $V \subseteq C$ be open with $Γ^{*} \subseteq V$ , and let $F$ be a primitive on $V$ of a continuous $f$ , so that $F^{'} = f$ is continuous (A primitive of a complex function on an open set). Then

$\int_{Γ} f (z) d z = 0.$

The hypothesis used is that the boundary function of $Γ$ vanishes, which is weaker than requiring every $γ_{k}$ to be closed.

Facts & Assumptions

Given: A cycle $Γ = \sum_{k < r} m_{k} γ_{k}$ with $γ_{k} : [a_{k}, b_{k}] \to C$ , an open $V \supseteq Γ^{*}$ , and a primitive $F$ on $V$ of a continuous $f$ with $F^{'} = f$ continuous.

[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$ (Integration over a complex chain and the index of a chain).

[L3]

If $F$ is a primitive of a continuous $f$ on an open set containing the trace of a rectifiable contour $γ : [a, b] \to C$ and $F^{'} = f$ is continuous, then $\int_{γ} f (z) d z = F (γ (b)) - F (γ (a))$ (The line integral of a continuous function admitting a primitive is that primitive's endpoint increment along every rectifiable path).

[L4]

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

[L5]

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

[L6]

A primitive of $f$ on $V$ is a holomorphic $F$ with $F^{'} = f$ on $V$ (A primitive of a complex function on an open set).

Proof

technique · direct

1.1

Write $K = {k < r : m_{k} \neq 0}$ and $Q = {γ_{k} (a_{k}) : k \in K} \cup {γ_{k} (b_{k}) : k \in K}$ , a finite subset of $Γ^{*} \subseteq V$ by [L1]; so $F$ is defined at every point of $Q$ .

givenL1L5L6

1.2

For every $k \in K$ the trace $γ_{k}^{*}$ lies in the open set $V$ on which $F$ is a primitive of the continuous $f$ with continuous $F^{'}$ , so [L3] gives $\int_{γ_{k}} f d z = F (γ_{k} (b_{k})) - F (γ_{k} (a_{k}))$ .

givenL1L3L6

2.1

By [L2] and step 1.2, $\int_{Γ} f d z = \sum_{k \in K} m_{k} F (γ_{k} (b_{k})) - \sum_{k \in K} m_{k} F (γ_{k} (a_{k}))$ , using [L4] to split the sum.

step 1.2L2L4

3.1

The index set $K$ is the disjoint union over $q \in Q$ of ${k \in K : γ_{k} (b_{k}) = q}$ , so [L5] and [L4] give $\sum_{k \in K} m_{k} F (γ_{k} (b_{k})) = \sum_{q \in Q} F (q) \sum {m_{k} : k \in K, γ_{k} (b_{k}) = q}$ , and likewise with $a_{k}$ in place of $b_{k}$ ; a term with $m_{k} = 0$ contributes $0$ to the boundary sums of [L1], so subtracting gives $\int_{Γ} f d z = \sum_{q \in Q} F (q) \partial Γ (q)$ .

step 1.1step 2.1L1L4L5

4.1

Every $\partial Γ (q)$ vanishes because $Γ$ is a cycle, so the sum of step 3.1 is $0$ , whence $\int_{Γ} f d z = 0$ ; the same conclusion holds for the empty cycle, whose defining sum is empty and therefore $0$ by [L5].

step 3.1L1L5∎

Depends on

Used by

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