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.
The polynomial ring over a commutative ring as finitely supported coefficient sequences with convolution
Definition
Let be a commutative ring (Commutative ring). A function has finite support when there is such that for every . The polynomial ring is the set of all finitely supported functions .
For and , define
The convolution sum is a finite sum in the additive commutative monoid of (A finite sum in a commutative monoid indexed by an arbitrary finite set). Write for the zero sequence, for the sequence with coefficient at index and zero elsewhere, and for the sequence with coefficient at index and zero elsewhere. The coefficient sequence supported at with value is denoted again by , and a polynomial is written formally as .
The closure of these operations and the commutative-ring axioms are established by Coefficientwise sums and convolution products of finitely supported sequences are finitely supported ↗ and Polynomial convolution makes a commutative ring containing as its constant subring ↗.