Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

α⋅β\alpha \cdot \beta is the order type of α×β\alpha \times \beta ordered by last differences, that is β\beta copies of α\alpha

Statement

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

(x,y)<(x′,y′) :  ⟺   y∈y′,  or  (y=y′ and x∈x′),(x, y) < (x', y') \ :\iff\ y \in y', \ \text{ or } \ \big(y = y' \text{ and } x \in x'\big),

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

ot(α⊗β)=α⋅β\mathrm{ot}(\alpha \otimes \beta) = \alpha \cdot \beta

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

No choice principle is used.

Facts & Assumptions

Given: Ordinals α\alpha and β\beta, and the ordered set α⊗β\alpha \otimes \beta described above. Ordinals carry the membership order and ot\mathrm{ot} 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)x < y \iff 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]

ot(W)=ot(I)+ot(W∖I)\mathrm{ot}(W) = \mathrm{ot}(I) + \mathrm{ot}(W \setminus I) for every well-order WW and every initial segment II of it (claim (b) of α+β\alpha + \beta is the order type of α\alpha followed by β\beta).

[L6]

α⋅0=0\alpha \cdot 0 = 0, α⋅δ+=α⋅δ+α\alpha \cdot \delta^{+} = \alpha \cdot \delta + \alpha, and α⋅λ=⋃{α⋅ξ:ξ∈λ}\alpha \cdot \lambda = \bigcup\{\alpha \cdot \xi : \xi \in \lambda\} for limit λ\lambda (Ordinal multiplication α⋅β\alpha \cdot \beta).

[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 PP of ordinals fails at some β0\beta_0, apply Transfinite induction to the well-order (β0+,∈)(\beta_0^{+}, \in) and to S={ξ∈β0+:P(ξ)}S = \{\xi \in \beta_0^{+} : P(\xi)\}; since every nonempty set of ordinals has an ∈\in-least element (Trichotomy and well-ordering of the ordinals) and the initial segment of β0+\beta_0^{+} below ξ\xi is ξ\xi, it follows that if PP holds at ξ\xi whenever it holds at every ordinal in ξ\xi, then PP holds at every ordinal.

[L9]

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

Proof

technique · direct
1.1

α⊗β\alpha \otimes \beta is a well-order: the relation is irreflexive, transitive and trichotomous because ∈\in is so on β\beta and on α\alpha and the rule compares second coordinates first; and a nonempty S⊆α×βS \subseteq \alpha \times \beta has a least element, obtained by taking y0y_0 the ∈\in-least second coordinate occurring in SS and then x0x_0 the ∈\in-least first coordinate with (x0,y0)∈S(x_0, y_0) \in S, both existing by [L2] applied inside β\beta and inside α\alpha.

L2L7construct
1.2

For an ordinal ξ\xi with ξ⊆β\xi \subseteq \beta the set α×ξ\alpha \times \xi is downward closed in α⊗β\alpha \otimes \beta, because (x′,y′)<(x,y)(x', y') < (x, y) with y∈ξy \in \xi gives y′∈yy' \in y or y′=yy' = y and hence y′∈ξy' \in \xi by transitivity of ξ\xi; and a downward closed subset JJ of an ordinal θ\theta is itself an ordinal, being transitive and strictly well ordered by ∈\in.

L4L7
2.1

Case β=0\beta = 0: α×0=∅\alpha \times 0 = \varnothing, whose order type is 0=α⋅00 = \alpha \cdot 0.

step 1.1L1L6
2.2

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

step 1.1step 1.2L1L3L5L6
2.3

Case β=λ\beta = \lambda a limit, assuming ot(α⊗ξ)=α⋅ξ\mathrm{ot}(\alpha \otimes \xi) = \alpha \cdot \xi for every ξ∈λ\xi \in \lambda: let gg be the order isomorphism of α⊗λ\alpha \otimes \lambda onto θ=ot(α⊗λ)\theta = \mathrm{ot}(\alpha \otimes \lambda); for ξ∈λ\xi \in \lambda the set α×ξ\alpha \times \xi is downward closed, so g[α×ξ]g[\alpha \times \xi] is downward closed in θ\theta and hence an ordinal by step 1.2, and gg restricts to an order isomorphism of α⊗ξ\alpha \otimes \xi onto it, giving g[α×ξ]=ot(α⊗ξ)=α⋅ξg[\alpha \times \xi] = \mathrm{ot}(\alpha \otimes \xi) = \alpha \cdot \xi; every point (x,y)(x,y) of α×λ\alpha \times \lambda lies in α×y+\alpha \times y^{+} with y+∈λy^{+} \in \lambda by [L9]; hence θ=g[α×λ]=⋃{g[α×ξ]:ξ∈λ}=⋃{α⋅ξ:ξ∈λ}=α⋅λ\theta = g[\alpha \times \lambda] = \bigcup\{g[\alpha \times \xi] : \xi \in \lambda\} = \bigcup\{\alpha \cdot \xi : \xi \in \lambda\} = \alpha \cdot \lambda.

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 β\beta from the claim at every ordinal in β\beta, so by [L8] ot(α⊗β)=α⋅β\mathrm{ot}(\alpha \otimes \beta) = \alpha \cdot \beta for all ordinals α\alpha and β\beta.

step 2.1step 2.2step 2.3L8L9
4.1

α⊗β\alpha \otimes \beta is therefore a well-order of order type α⋅β\alpha \cdot \beta.

step 3.1step 1.1∎

Remarks

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

The two standard computations. 2⋅ω2 \cdot \omega is ω\omega copies of a two element set, which is a copy of ω\omega; ω⋅2\omega \cdot 2 is two copies of ω\omega, which is ω+ω\omega + \omega. 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 α+β\alpha + \beta is the order type of α\alpha followed by β\beta: cutting the product at the last copy of α\alpha 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 · next 3 levels

Direct dependencies and their dependencies through the next three levels: 49 results over 22 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources