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 product of a finite list in a monoid, by recursion, with the empty product () equal to the identity
Definition
Let be a monoid (Semigroup and monoid) and let be a family of elements of , written . There is exactly one function satisfying
and we write
In particular the empty product is , and .
Why the recursion is legitimate. The clause consults as well as , so The recursion theorem does not apply to it directly. Apply that theorem instead with the set , the element , and the function given by : it yields a unique with and . Writing , induction (The principle of mathematical induction) gives for every , since and . Hence , so satisfies the two displayed equations. It is the only such function: if satisfies them too, then contains and is closed under , hence is all of by induction.
The value depends only on . If satisfy for every , then . Indeed the set of for which this implication holds contains , both products then being ; and if it holds at , and agree at every , then they agree at every and also at itself, because is equivalent to (On the order is membership: ), so . Induction finishes it. This is what makes the notation unambiguous: it names a value determined by the first terms alone, and a finite list of length , that is a function on the von Neumann natural (The natural numbers (von Neumann)), determines the product computed from any extension of .
Remarks
-
The empty product is the identity, and this is not a convention chosen for convenience. It is forced by the recursion, whose base clause is , and it is what makes the induction in Generalised associativity: in a monoid the product of a finite list does not depend on the bracketing, and in a commutative monoid it does not depend on the order of the factors either start. contains (The natural numbers (von Neumann)), so is a genuine case of every statement below, never an afterthought.
-
The factors are multiplied left to right: appends on the right. Nothing depends on that choice, because Generalised associativity: in a monoid the product of a finite list does not depend on the bracketing, and in a commutative monoid it does not depend on the order of the factors either shows the value is unchanged by any regrouping of consecutive factors; but the choice must be made, since the recursion has to say where the new factor goes.
-
The existing Finite sums and finite products, by recursion is a different object: it is stated for sequences in the complete ordered field, and its multiplicative alias already names the product of real numbers. It cannot carry a product in an arbitrary monoid, which is why this item exists.