LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-29

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.

$α \cdot β$ is the order type of $α \times β$ ordered by last differences, that is $β$ copies of $α$

Statement

Let $α$ and $β$ be ordinals (Ordinal (von Neumann)). Order the Cartesian product $α \times β$ by last differences:

$(x, y) < (x^{'}, y^{'}) : ⟺ y \in y^{'}, or (y = y^{'} and x \in x^{'}),$

so the second coordinate is compared first and the first coordinate only breaks a tie. Write $α \otimes β$ for the resulting ordered set. Then $α \otimes β$ is a well-order (Well-order and well-ordered set) and

$o t (α \otimes β) = α \cdot β$

(Every well-order has a unique order type, Ordinal multiplication $α \cdot β$ ). In words: $α \cdot β$ is $β$ copies of $α$ , laid end to end in the order given by $β$ , one copy $α \times {y}$ for each $y \in β$ .

No choice principle is used.

Facts & Assumptions

Given: Ordinals $α$ and $β$ , and the ordered set $α \otimes β$ described above. Ordinals carry the membership order and $o t$ denotes order type.

[L1]

Every well-order is order isomorphic to exactly one ordinal, its order type, and order isomorphic well-orders have the same order type (Every well-order has a unique order type).

[L2]

A well-order is a total order in which every nonempty subset has a least element (Well-order and well-ordered set).

[L3]

An order isomorphism is a bijection with $x < y ⟺ f (x) < f (y)$ ; a strictly increasing bijection between total orders is one; and the restriction of an order isomorphism to a subset is an order isomorphism onto the image (Order embedding and order isomorphism).

[L4]

An initial segment is a downward closed subset, and every initial segment of a well-order is itself a well-order (Initial segment of a well-order).

[L5]

$o t (W) = o t (I) + o t (W ∖ I)$ for every well-order $W$ and every initial segment $I$ of it (claim (b) of $α + β$ is the order type of $α$ followed by $β$ ).

[L6]

$α \cdot 0 = 0$ , $α \cdot δ^{+} = α \cdot δ + α$ , and $α \cdot λ = ⋃ {α \cdot ξ : ξ \in λ}$ for limit $λ$ (Ordinal multiplication $α \cdot β$ ).

[L7]

An ordinal is a transitive set strictly well ordered by $\in$ , and every element of an ordinal is an ordinal (Ordinal (von Neumann), Basic closure properties of ordinals).

[L8]

Transfinite induction over the ordinals: if a property $P$ of ordinals fails at some $β_{0}$ , apply Transfinite induction to the well-order $(β_{0}^{+}, \in)$ and to $S = {ξ \in β_{0}^{+} : P (ξ)}$ ; since every nonempty set of ordinals has an $\in$ -least element (Trichotomy and well-ordering of the ordinals) and the initial segment of $β_{0}^{+}$ below $ξ$ is $ξ$ , it follows that if $P$ holds at $ξ$ whenever it holds at every ordinal in $ξ$ , then $P$ holds at every ordinal.

[L9]

Every ordinal is exactly one of $0$ , a successor, or a limit; a nonzero ordinal $λ$ is a limit if and only if $ξ \in λ$ implies $ξ^{+} \in λ$ (Successor and limit ordinals).

Proof

technique · direct

1.1

$α \otimes β$ is a well-order: the relation is irreflexive, transitive and trichotomous because $\in$ is so on $β$ and on $α$ and the rule compares second coordinates first; and a nonempty $S \subseteq α \times β$ has a least element, obtained by taking $y_{0}$ the $\in$ -least second coordinate occurring in $S$ and then $x_{0}$ the $\in$ -least first coordinate with $(x_{0}, y_{0}) \in S$ , both existing by [L2] applied inside $β$ and inside $α$ .

L2L7construct

1.2

For an ordinal $ξ$ with $ξ \subseteq β$ the set $α \times ξ$ is downward closed in $α \otimes β$ , because $(x^{'}, y^{'}) < (x, y)$ with $y \in ξ$ gives $y^{'} \in y$ or $y^{'} = y$ and hence $y^{'} \in ξ$ by transitivity of $ξ$ ; and a downward closed subset $J$ of an ordinal $θ$ is itself an ordinal, being transitive and strictly well ordered by $\in$ .

L4L7

2.1

Case $β = 0$ : $α \times 0 = \emptyset$ , whose order type is $0 = α \cdot 0$ .

step 1.1L1L6

2.2

Case $β = δ^{+}$ , assuming $o t (α \otimes δ) = α \cdot δ$ : the set $α \times δ$ is an initial segment of $α \otimes δ^{+}$ by step 1.2, its complement is $α \times {δ}$ , and $(x, δ) \mapsto x$ is an order isomorphism of that complement onto $α$ , since two points of it are compared by their first coordinates; and $o t (α) = α$ , because the identity is an order isomorphism and order types are unique by [L1]; so [L5] gives $o t (α \otimes δ^{+}) = o t (α \otimes δ) + o t (α) = α \cdot δ + α = α \cdot δ^{+}$ .

step 1.1step 1.2L1L3L5L6

2.3

Case $β = λ$ a limit, assuming $o t (α \otimes ξ) = α \cdot ξ$ for every $ξ \in λ$ : let $g$ be the order isomorphism of $α \otimes λ$ onto $θ = o t (α \otimes λ)$ ; for $ξ \in λ$ the set $α \times ξ$ is downward closed, so $g [α \times ξ]$ is downward closed in $θ$ and hence an ordinal by step 1.2, and $g$ restricts to an order isomorphism of $α \otimes ξ$ onto it, giving $g [α \times ξ] = o t (α \otimes ξ) = α \cdot ξ$ ; every point $(x, y)$ of $α \times λ$ lies in $α \times y^{+}$ with $y^{+} \in λ$ by [L9]; hence $θ = g [α \times λ] = ⋃ {g [α \times ξ] : ξ \in λ} = ⋃ {α \cdot ξ : ξ \in λ} = α \cdot λ$ .

step 1.1step 1.2L1L3L6L9

3.1

The three cases of [L9] are exhaustive, and each of steps 2.1, 2.2 and 2.3 derives the claim at $β$ from the claim at every ordinal in $β$ , so by [L8] $o t (α \otimes β) = α \cdot β$ for all ordinals $α$ and $β$ .

step 2.1step 2.2step 2.3L8L9

4.1

$α \otimes β$ is therefore a well-order of order type $α \cdot β$ .

step 3.1step 1.1∎

Remarks

Why last differences and not first differences. With the order above, the copy $α \times {y}$ sits below the copy $α \times {y^{'}}$ whenever $y \in y^{'}$ , so the picture is " $β$ copies of $α$ ", matching the successor clause $α \cdot δ^{+} = α \cdot δ + α$ of Ordinal multiplication $α \cdot β$ , which appends a copy of $α$ on the right. Ordering by first differences would give " $α$ copies of $β$ ", which is the product under the opposite convention and is a different ordinal in general.

The two standard computations. $2 \cdot ω$ is $ω$ copies of a two element set, which is a copy of $ω$ ; $ω \cdot 2$ is two copies of $ω$ , which is $ω + ω$ . Both are carried out in FALSE: ordinal multiplication is commutative, and they are the shortest possible demonstration that ordinal multiplication is not commutative.

Where the sum lemma enters. Only at step 2.2, through clause (b) of $α + β$ is the order type of $α$ followed by $β$ : cutting the product at the last copy of $α$ splits it into an initial segment and a remainder, and the order type of a split is the sum of the two order types. The limit case needs no such cut, only that the initial pieces exhaust the whole.

Depends on

Used by

Dependency tree · two levels

24 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Ordinal arithmetic (Wikipedia) (standard reference, not scraped)
Order type (Wikipedia) (standard reference, not scraped)
T. Jech, Set Theory, 3rd millennium ed., Ch. 2 (Ordinal numbers) (standard reference, not scraped)
Open Logic Project, Open Logic Text (standard reference, not scraped)

α⋅βα⋅β is the order type of α×βα×β ordered by last differences, that is ββ copies of αα