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.
Real singular cochain complex
Definition
For a topological space , the real singular cochain complex is Here the chains and boundary are Real singular chain complex, so for . Addition and scalar multiplication of cochains are pointwise. Precomposition with the real-linear boundary is real-linear. Explicitly, for , There is no extra degree sign. For every chain , , so . The same assertion in negative degrees follows from the zero source, including .
By Real singular cochains identify with functions on the supplied simplex basis, evaluation on the supplied basis identifies this with Singular cochain complex with coefficients for coefficient group : it is , not . That lemma verifies the identification commutes with coboundary. A cochain may have arbitrary values on infinitely many simplices; it is not required to have finite support.
At degree zero a cochain is a function on points, and its coboundary on a path is the final value minus the initial value. For the empty space all cochains vanish. For a point the unnormalized cochain groups are in each nonnegative degree, with for even and for odd . No choice is involved.