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.
Complex chains, their traces, and cycles
Definition
Let be open. A complex chain in is a finite list
each an integer (The integers as equivalence classes of pairs of naturals) and each a complex contour (Rectifiable complex contours, reversal, concatenation, closedness, and orientation) whose trace lies in . It is written . The list of length is the empty chain.
Its trace is the set
a subset of ; a term with contributes nothing to it.
Its boundary is the function given by
each sum being a finite sum over a subset of (A finite sum in a commutative monoid indexed by an arbitrary finite set, The cardinality of a finite set), and the subtraction is that of the commutative ring (The integers form a commutative ring). The chain is a cycle when for every .
Sum and negation. For chains and in , the sum is the concatenated list, and is the list with every coefficient replaced by and every contour unchanged. Write . The reversal is the list with every coefficient unchanged and every contour replaced by its reversal; the additive inverse is taken in (The integers form a commutative ring).
Remarks
A chain is a list, and equality of chains is equality of lists. No free abelian group on the set of contours is introduced here, and no result on this page asserts that two differently presented chains are equal: every statement below is about a given list, and the operations above produce lists. This is a deliberate departure from the presentations that define a chain as a group element, and it is what removes the obligation to say when two chains coincide.
Which lists are cycles. The empty chain is a cycle, both boundary sums being empty and hence (A finite sum in a commutative monoid indexed by an arbitrary finite set). A list all of whose contours are closed is a cycle: for such a the two endpoint values coincide, so enters the sum at once positively and once negatively and cancels there, and enters neither sum at any other point. In particular a single closed contour, taken as the list of length with , is a cycle. Terms with add to both sums and so never affect .
Cycles are more general than lists of closed contours. The condition is that the endpoints cancel after the coefficients are counted, not that each piece closes up: two contours with the same initial point and the same terminal point, carried with coefficients and , form a cycle although neither is closed. The distinction is what the integral results below actually use: the vanishing of the boundary function is exactly the hypothesis under which the integral of a continuous derivative over is zero.
Ambient set. A chain is a chain in ; the same list is a chain in every open set containing all the , and in particular in . When a nonempty connected is wanted it is called a complex domain (A complex domain is a nonempty connected open subset of ). Finite sums of integers and of complex numbers are finite sums in their additive commutative monoids, as in A finite sum in a commutative monoid indexed by an arbitrary finite set.
Depends on
Rectifiable complex contours, reversal, concatenation, closedness, and orientation
Finite sums and finite products, by recursion
Laws of finite sums and finite products
A finite sum in a commutative monoid indexed by an arbitrary finite set
A complex domain is a nonempty connected open subset of
The integers as equivalence classes of pairs of naturals
The cardinality of a finite set
The integers form a commutative ring