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.
Null-homologous cycles and homologous cycles in an open set
Definition
Let be open and let be a complex chain which is a cycle and whose trace lies in (Complex chains, their traces, and cycles).
is null-homologous in when
the index being that of Integration over a complex chain and the index of a chain; the values are defined because , so every lies off the trace, and they are integers by The index of a cycle about a point off its trace is an integer.
Two cycles with traces in are homologous in when is null-homologous in . By Chain integration and the index are additive in the chain, and reverse with it the chain is again a cycle with trace inside , and its index at a point off that union is ; so the condition says exactly that
Remarks
Both notions depend on , not on the cycle alone. The same cycle can be null-homologous in one open set and not in another: enlarging removes points from and so weakens the requirement. Every statement below that uses these words names the open set it uses them in, and is not omitted anywhere.
Null-homologous does not mean equal to the empty chain. It is a condition on the numbers for outside , and a cycle with a large trace can satisfy it. In particular, being homologous is a relation between two cycles and never an assertion that the two lists coincide; chains here are lists and equality of chains is equality of lists.
Taking makes the condition vacuous, since is empty, so every cycle is null-homologous in the plane. The content of the notion appears when omits points, and it is those omitted points that the index has to ignore. When a nonempty connected is wanted it is called a complex domain (A complex domain is a nonempty connected open subset of ).