Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: 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.

2⋅ω=ω2 \cdot \omega = \omega while ω⋅2=ω+ω\omega \cdot 2 = \omega + \omega, pictured as order types

Example

2⋅ω=ω,ω⋅2=ω+ω>ω.2 \cdot \omega = \omega, \qquad \omega \cdot 2 = \omega + \omega > \omega.

Under the convention of Ordinal multiplication α⋅β\alpha \cdot \beta, α⋅β\alpha \cdot \beta is β\beta copies of α\alpha (α⋅β\alpha \cdot \beta is the order type of α×β\alpha \times \beta ordered by last differences, that is β\beta copies of α\alpha). So 2⋅ω2 \cdot \omega is ω\omega copies of a two element set, laid end to end:

∙ ∙⏟  ∙ ∙⏟  ∙ ∙⏟  ⋯\underbrace{\bullet\ \bullet}_{}\ \ \underbrace{\bullet\ \bullet}_{}\ \ \underbrace{\bullet\ \bullet}_{}\ \ \cdots

which is a copy of ω\omega once the points are counted off 0,1,2,…0, 1, 2, \dots. And ω⋅2\omega \cdot 2 is two copies of ω\omega, one entirely above the other:

0,1,2,…  then  0′,1′,2′,…0, 1, 2, \dots \ \ \text{then} \ \ 0', 1', 2', \dots

which is ω+ω\omega + \omega and is strictly larger than ω\omega.

Both values are computed below from the recursive clauses, and both pictures are justified by the order-type lemmas rather than left as pictures.

Facts & Assumptions

Given: The ordinals with the operations of Ordinal addition α+β\alpha + \beta and Ordinal multiplication α⋅β\alpha \cdot \beta, and ω\omega the least limit ordinal (ω\omega is the least limit ordinal, The natural numbers N\mathbb{N} (von Neumann)).

[L1]

α⋅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); α+0=α\alpha + 0 = \alpha (Ordinal addition α+β\alpha + \beta).

[L2]

From Monotonicity of ordinal ++ and ⋅\cdot: strictly increasing and continuous in the right argument, weakly increasing in the left, with left cancellation, and the identities 0+β=β0 + \beta = \beta and 1⋅β=β1 \cdot \beta = \beta: 1⋅μ=μ⋅1=μ1 \cdot \mu = \mu \cdot 1 = \mu (claim (a)); ν<θ\nu < \theta implies α+ν<α+θ\alpha + \nu < \alpha + \theta (claim (b)); μ≤ν\mu \le \nu implies μγ≤νγ\mu\gamma \le \nu\gamma (claim (e)).

[L3]

For m,n∈ωm, n \in \omega the ordinal m⋅nm \cdot n lies in ω\omega (claim (a) of On ω\omega the ordinal ++ and ⋅\cdot are the Peano operations: ω\omega is closed under ordinal ++, ⋅\cdot and exponentiation, and for naturals m,nm, n the ordinal m+nm + n and m⋅nm \cdot n are the natural-number sum and product).

[L4]

ω\omega is a limit ordinal, so ⋃ω=ω\bigcup \omega = \omega and 0∈ω0 \in \omega (ω\omega is the least limit ordinal, Successor and limit ordinals); every ordinal is transitive, μ⊆ν\mu \subseteq \nu iff μ∈ν\mu \in \nu or μ=ν\mu = \nu, and μ∉μ\mu \notin \mu (Ordinal (von Neumann), Basic closure properties of ordinals, Trichotomy and well-ordering of the ordinals).

[L5]

α⋅β\alpha \cdot \beta is the order type of α×β\alpha \times \beta under last differences, that is β\beta copies of α\alpha (α⋅β\alpha \cdot \beta is the order type of α×β\alpha \times \beta ordered by last differences, that is β\beta copies of α\alpha); α+β\alpha + \beta is the order type of a copy of α\alpha followed by a copy of β\beta (α+β\alpha + \beta is the order type of α\alpha followed by β\beta); order types are unique (Every well-order has a unique order type) and a strictly increasing bijection between total orders is an order isomorphism (Order embedding and order isomorphism).

Verification

technique · direct
1.1

For n∈ωn \in \omega the ordinal 2⋅n2 \cdot n lies in ω\omega by [L3], hence 2⋅n⊆ω2 \cdot n \subseteq \omega by [L4]; and n=1⋅n≤2⋅nn = 1 \cdot n \le 2 \cdot n by [L2], since 1≤21 \le 2, hence n⊆2⋅nn \subseteq 2 \cdot n.

L2L3L4
1.2

ω⋅2=ω⋅1+=ω⋅1+ω=ω+ω\omega \cdot 2 = \omega \cdot 1^{+} = \omega \cdot 1 + \omega = \omega + \omega by [L1] and [L2]; and ω+ω>ω+0=ω\omega + \omega > \omega + 0 = \omega by [L1] and claim (b) of [L2], since 0∈ω0 \in \omega.

L1L2L4
2.1

2⋅ω=⋃{2⋅n:n∈ω}2 \cdot \omega = \bigcup\{2 \cdot n : n \in \omega\} by [L1], and this equals ω\omega: it is contained in ω\omega by step 1.1, and it contains ⋃{n:n∈ω}=⋃ω=ω\bigcup\{n : n \in \omega\} = \bigcup \omega = \omega by step 1.1 and [L4].

step 1.1L1L4
3.1

The pictures are the order-type lemmas, not extra assumptions: by [L5], 2⋅ω2 \cdot \omega is the order type of 2×ω2 \times \omega under last differences, which is ω\omega blocks of two, and step 2.1 evaluates that order type as ω\omega; while ω⋅2\omega \cdot 2 is the order type of ω×2\omega \times 2 under last differences, which is two blocks of ω\omega, and by [L5] again that is the order type of a copy of ω\omega followed by a copy of ω\omega, namely ω+ω\omega + \omega, in agreement with step 1.2.

step 2.1step 1.2L5
4.1

Therefore 2⋅ω=ω2 \cdot \omega = \omega and ω⋅2=ω+ω≠ω\omega \cdot 2 = \omega + \omega \ne \omega, so the two products differ.

step 2.1step 3.1step 1.2∎

Remarks

Which convention this depends on. Everything above uses the convention fixed in Ordinal multiplication α⋅β\alpha \cdot \beta, that the successor clause appends a copy of the left factor on the right. Under the opposite convention the two values are exchanged, and 2⋅ω2 \cdot \omega would be ω+ω\omega + \omega. Both conventions appear in the literature; this library uses the one stated, throughout.

The general statement. That ordinal multiplication is not commutative is FALSE: ordinal multiplication is commutative, whose refutation is the computation of step 2.1 and step 1.2. The related failure of right distributivity, (1+1)⋅ω≠1⋅ω+1⋅ω(1+1) \cdot \omega \ne 1 \cdot \omega + 1 \cdot \omega, is FALSE: (β+γ)⋅α=β⋅α+γ⋅α(\beta + \gamma)\cdot\alpha = \beta\cdot\alpha + \gamma\cdot\alpha for all ordinals and uses the same value 2⋅ω=ω2 \cdot \omega = \omega.

Why the block picture is a proof and not an illustration. α⋅β\alpha \cdot \beta is the order type of α×β\alpha \times \beta ordered by last differences, that is β\beta copies of α\alpha says the product is the order type of the block arrangement, so reading a value off the picture is legitimate once the picture is identified with α×β\alpha \times \beta under last differences. What is not legitimate is reading it off an unlabelled diagram, which is why step 3.1 names the lemma at each use.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 61 results over 28 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