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.
Holomorphic integrals agree on homologous cycles
Statement
Let be open, let be holomorphic, and let be complex chains which are cycles with traces in and which are homologous in (Null-homologous cycles and homologous cycles in an open set). Then
Facts & Assumptions
Given: An open , a holomorphic , and cycles with traces in , homologous in .
If is a cycle with trace in an open , null-homologous in , and is holomorphic on , then (Cauchy's theorem for a null-homologous cycle).
Two cycles with traces in are homologous in when their difference is null-homologous in (Null-homologous cycles and homologous cycles in an open set).
and ; the sum of two cycles and the negative of a cycle are cycles; and for continuous on the traces involved, and (Chain integration and the index are additive in the chain, and reverse with it).
(Integration over a complex chain and the index of a chain), a chain being a finite list of integer-weighted complex contours (Complex chains, their traces, and cycles).
A complex differentiable function is continuous (Complex differentiability at a point implies continuity there).
Proof
By [L3] the chain is a cycle and its trace is , which lies in ; and is continuous on that trace by [L5].
By [L2] the chain is null-homologous in , since and are homologous there.
Steps 1.1 and 1.2 put under the hypotheses of [L1], so .
By [L3] the left-hand side of step 2.1 equals , so the two integrals agree.
Depends on
Cauchy's theorem for a null-homologous cycle
Null-homologous cycles and homologous cycles in an open set
Chain integration and the index are additive in the chain, and reverse with it
Integration over a complex chain and the index of a chain
Complex chains, their traces, and cycles
Complex differentiability at a point implies continuity there