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.
Series in the nonnegative extended real line
Definition
Let take values in (The extended real line , its order, and the arithmetic that is left undefined). Its partial sums are the unique sequence in satisfying
To apply The recursion theorem with a fixed successor function, use the state space and the self-map , starting from . Recursion gives a unique state sequence; induction makes its first coordinate , and its second coordinates are exactly the unique satisfying the displayed recurrence. Addition of two nonnegative extended reals is always defined, including when either is . The sequence is nondecreasing, and its nonnegative extended sum is
whose existence follows from completeness of the extended real line (Every subset of has a least upper bound and a greatest lower bound in , agreeing with the real supremum and infimum on nonempty sets bounded in ). More generally, for ,
Finite sums use the same recursion: , so the empty sum at is . A double sum such as means that the inner nonnegative extended sum is formed first and the resulting nonnegative extended sequence is then summed.