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.
Ordinal multiplication
Definition
Let and be ordinals (Ordinal (von Neumann)). The product , also written , is defined by recursion on , in the three cases of Successor and limit ordinals:
with the ordinal addition of Ordinal addition . That exactly one operation satisfies these three clauses, and that all its values are ordinals, is Ordinal multiplication exists and is unique, and its values are ordinals, proved immediately above. The union in the limit clause is the least upper bound of the values already produced (claim (e) of Basic closure properties of ordinals).
The convention, stated where it is made. The successor clause appends a copy of on the right, so is " copies of ", laid end to end in the order given by . Made precise, this is is the order type of ordered by last differences, that is copies of : is the order type of ordered by last differences, that is, by comparing the -coordinate first and using the -coordinate only to break a tie.
Both conventions occur in the literature and they give genuinely different operations, since multiplication is not commutative. Under the one adopted here while ; under the opposite convention those two values are exchanged. This library always uses the convention above, which is the one of Jech and of the Wikipedia article cited below.
Remarks
-
Why and not . The empty concatenation of copies of is empty. The multiplicative unit appears one clause later: , and is proved in Monotonicity of ordinal and : strictly increasing and continuous in the right argument, weakly increasing in the left, with left cancellation, and the identities and , so .
-
The limit clause is a supremum, and it is where the product loses commutativity. , and each is a finite ordinal, so the supremum is ; whereas , which is strictly larger. Both computations are carried out in FALSE: ordinal multiplication is commutative.
-
Notation. abbreviates , and the product binds tighter than the sum, so means . Ordinal expressions in this library are always written with that convention.
-
Agreement with the natural numbers. Below the limit clause never fires, and the two remaining clauses are literally the Peano clauses for multiplication on . That the ordinal product of two natural numbers is their natural-number product is On the ordinal and are the Peano operations: is closed under ordinal , and exponentiation, and for naturals the ordinal and are the natural-number sum and product.