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.
Integration over a complex chain and the index of a chain
Definition
Let be a complex chain (Complex chains, their traces, and cycles) with trace , and let be continuous on . The integral of over is
a finite sum (A finite sum in a commutative monoid indexed by an arbitrary finite set) of the complex line integrals of The complex line integral over a rectifiable path as a componentwise Riemann–Stieltjes integral. Each summand exists: for with the trace is contained in , so is continuous on it, and is rectifiable, so Continuous integrands have complex and absolute line integrals along every rectifiable path applies. Terms with are omitted, so no integral of over a contour outside the trace is required. The empty chain, and any chain all of whose coefficients vanish, give .
For , the index of about is
This is defined: is complex differentiable, hence continuous, on by Linearity, product, reciprocal, and quotient rules for complex derivatives and Complex differentiability at a point implies continuity there.
Remarks
The notation is consistent with the single-contour case. If , and is closed, then , the sum has the one term , and is the winding number of The winding number of a closed contour about a point off its trace for every . So writing for both costs no ambiguity.
Linearity in the integrand is inherited termwise from Complex line integrals are linear in the integrand, finite sums in the additive commutative monoid of (A finite sum in a commutative monoid indexed by an arbitrary finite set), and distributivity in the complex field ( is a field, every element is uniquely , and every nonzero element has inverse ): for continuous on and , .
The index is not defined on the trace. For the integrand is undefined at , and no value is assigned; every statement about below carries the hypothesis .
Depends on
Complex chains, their traces, and cycles
The winding number of a closed contour about a point off its trace
The complex line integral over a rectifiable path as a componentwise Riemann–Stieltjes integral
Continuous integrands have complex and absolute line integrals along every rectifiable path
Complex line integrals are linear in the integrand
A finite sum in a commutative monoid indexed by an arbitrary finite set
is a field, every element is uniquely , and every nonzero element has inverse
Linearity, product, reciprocal, and quotient rules for complex derivatives
Complex differentiability at a point implies continuity there