ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck 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.

The Cantor normal form of $(ω^{2} + ω \cdot 3 + 5) \cdot ω^{2}$ , computed by the division algorithm

Example

Put $α = ω^{2} + ω \cdot 3 + 5$ , which is already in Cantor normal form (Cantor normal form: every nonzero ordinal is $ω^{β_{0}} \cdot c_{0} + \dots + ω^{β_{k - 1}} \cdot c_{k - 1}$ with $β_{0} > \dots > β_{k - 1}$ and each $c_{i}$ a nonzero natural number, in exactly one way): the exponents $2 > 1 > 0$ strictly decrease and the coefficients $1, 3, 5$ are nonzero natural numbers, since $ω \cdot 3 = ω^{1} \cdot 3$ and $5 = ω^{0} \cdot 5$ . Then

$α \cdot ω^{2} = ω^{4},$

whose Cantor normal form is $ω^{4} \cdot 1$ : the entire tail $ω \cdot 3 + 5$ is annihilated by multiplying on the right by $ω^{2}$ . Multiplying on the right by a limit ordinal keeps only the leading behaviour.

Addition behaves quite differently. Also computed below:

$(ω^{2} + ω \cdot 3 + 5) + (ω \cdot 2 + 7) = ω^{2} + ω \cdot 5 + 7,$

where the coefficients of the matching power add and the lower tail of the left summand is swallowed.

Facts & Assumptions

Given: $α = ω^{2} + ω \cdot 3 + 5$ , with the operations of Ordinal addition $α + β$ , Ordinal multiplication $α \cdot β$ and Ordinal exponentiation $α^{β}$ , with the conventions $α^{0} = 1$ and $0^{0} = 1$ ; the finite ordinals $2, 3, 4, 5, 7$ are elements of $ω$ (The natural numbers $N$ (von Neumann), $ω$ is the least limit ordinal). Products bind tighter than sums, so $ω \cdot 3 + 5$ is $(ω \cdot 3) + 5$ .

[L1]

$α \cdot δ^{+} = α \cdot δ + α$ and $α \cdot λ = \sup {α \cdot ξ : ξ \in λ}$ for limit $λ$ (Ordinal multiplication $α \cdot β$ ); $α^{δ^{+}} = α^{δ} \cdot α$ and $α^{0} = 1$ (Ordinal exponentiation $α^{β}$ , with the conventions $α^{0} = 1$ and $0^{0} = 1$ ); $μ + 0 = μ$ , $μ + δ^{+} = (μ + δ)^{+}$ and $μ + λ = \sup {μ + ξ : ξ \in λ}$ for limit $λ$ (Ordinal addition $α + β$ ).

[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 + β = β$ and $1 \cdot β = β$ : $1 \cdot μ = μ \cdot 1 = μ$ and $0 + μ = μ$ (claim (a)); $ν < θ$ implies $μ + ν < μ + θ$ (claim (b)); for $μ > 0$ , $ν < θ$ implies $μ ν < μ θ$ (claim (d)); $μ \leq ν$ implies $μ γ \leq ν γ$ (claim (e)); $μ + λ = \sup {μ + ξ : ξ \in λ}$ and $μ \cdot λ = \sup {μ η : η \in D}$ for $μ > 0$ , $λ$ a limit and $D \subseteq λ$ nonempty with $\sup D = λ$ (claim (f)).

[L3]

$\cdot$ is associative and $μ (ν + θ) = μ ν + μ θ$ (Ordinal multiplication is associative, and $α \cdot (β + γ) = α \cdot β + α \cdot γ$ ); $+$ is associative (Ordinal addition is associative).

[L4]

$α^{β + γ} = α^{β} \cdot α^{γ}$ , $α^{1} = α$ , and for $α > 1$ the map $β \mapsto α^{β}$ is strictly increasing ( $α^{β + γ} = α^{β} \cdot α^{γ}$ and $(α^{β})^{γ} = α^{β \cdot γ}$ ; and for $α > 1$ exponentiation is strictly increasing with $β \leq α^{β}$ ).

[L5]

For $μ > 0$ every $ν$ is $μ \cdot ξ + ρ$ with $ρ < μ$ , uniquely (For $α > 0$ every ordinal $β$ is $α \cdot ξ + ρ$ with $ρ < α$ , in exactly one way); every nonzero ordinal has exactly one Cantor normal form (Cantor normal form: every nonzero ordinal is $ω^{β_{0}} \cdot c_{0} + \dots + ω^{β_{k - 1}} \cdot c_{k - 1}$ with $β_{0} > \dots > β_{k - 1}$ and each $c_{i}$ a nonzero natural number, in exactly one way).

[L6]

For $m, n \in ω$ the ordinals $m + n$ and $m \cdot n$ lie in $ω$ and agree with the natural-number sum and product (On $ω$ the ordinal $+$ and $\cdot$ are the Peano operations: $ω$ is closed under ordinal $+$ , $\cdot$ and exponentiation, and for naturals $m, n$ the ordinal $m + n$ and $m \cdot n$ are the natural-number sum and product).

[L7]

$ω$ is a limit ordinal with $⋃ ω = ω$ ( $ω$ is the least limit ordinal, Successor and limit ordinals); every ordinal is transitive, $μ \subseteq ν$ iff $μ \in ν$ or $μ = ν$ , and trichotomy holds (Ordinal (von Neumann), Basic closure properties of ordinals, Trichotomy and well-ordering of the ordinals).

Verification

technique · direct

1.1

Preliminary identities: $ω^{1} = ω$ and $ω^{2} = ω^{1^{+}} = ω^{1} \cdot ω = ω \cdot ω$ by [L1] and [L4]; $ω \cdot 3 + ω = ω \cdot 3^{+} = ω \cdot 4$ , $ω + ω = ω \cdot 1 + ω = ω \cdot 1^{+} = ω \cdot 2$ , and $ω^{2} + ω^{2} = ω^{2} \cdot 1 + ω^{2} = ω^{2} \cdot 2$ by [L1] and [L2].

L1L2L4

1.2

For $n \in ω$ the ordinals $2 \cdot n$ and $5 + n$ lie in $ω$ by [L6], hence are subsets of $ω$ by [L7]; and $n = 1 \cdot n \leq 2 \cdot n$ and $n \leq 5 + n$ by [L2], so both ${2 \cdot n : n \in ω}$ and ${5 + n : n \in ω}$ are nonempty subsets of $ω$ with supremum $⋃ ω = ω$ .

L2L6L7

2.1

$ω^{2} \leq α < ω^{2} \cdot 2$ : the first inequality is $ω^{2} = ω^{2} + 0 \leq ω^{2} + (ω \cdot 3 + 5)$ by [L1] and [L2]; for the second, $5 < ω$ gives $ω \cdot 3 + 5 < ω \cdot 3 + ω = ω \cdot 4$ by [L2] and step 1.1, and $4 < ω$ with $ω > 0$ gives $ω \cdot 4 < ω \cdot ω = ω^{2}$ by [L2] and step 1.1, so $α < ω^{2} + ω^{2} = ω^{2} \cdot 2$ by [L2] and step 1.1.

step 1.1L1L2L7

2.2

The addition: $5 + ω = \sup {5 + n : n \in ω} = ω$ by [L1] and step 1.2, so $5 + ω \cdot 2 = 5 + (ω + ω) = (5 + ω) + ω = ω + ω = ω \cdot 2$ using [L3] and step 1.1; hence $α + (ω \cdot 2 + 7) = ω^{2} + ω \cdot 3 + (5 + ω \cdot 2) + 7 = ω^{2} + (ω \cdot 3 + ω \cdot 2) + 7 = ω^{2} + ω \cdot (3 + 2) + 7 = ω^{2} + ω \cdot 5 + 7$ , the regrouping by [L3], the last product by left distributivity in [L3] and $3 + 2 = 5$ by [L6].

step 1.2step 1.1L1L3L6

3.1

$α \cdot ω = ω^{3}$ : by [L1], $α \cdot ω = \sup {α \cdot n : n \in ω}$ , and step 2.1 with claim (e) of [L2] gives $ω^{2} \cdot n \leq α \cdot n \leq (ω^{2} \cdot 2) \cdot n = ω^{2} \cdot (2 \cdot n)$ for every $n \in ω$ , using associativity of $\cdot$ from [L3]; the suprema of the outer two families are both $ω^{2} \cdot ω$ , the first by [L1] and the second by claim (f) of [L2] applied to the set ${2 \cdot n : n \in ω}$ , which is unbounded in $ω$ by step 1.2; so $α \cdot ω = ω^{2} \cdot ω = ω^{2} \cdot ω^{1} = ω^{2 + 1} = ω^{3}$ by [L4].

step 2.1step 1.2step 1.1L1L2L3L4

4.1

$α \cdot ω^{2} = ω^{4}$ : by step 1.1, $ω^{2} = ω \cdot ω$ , so associativity in [L3] gives $α \cdot ω^{2} = α \cdot (ω \cdot ω) = (α \cdot ω) \cdot ω = ω^{3} \cdot ω = ω^{3} \cdot ω^{1} = ω^{3 + 1} = ω^{4}$ by step 3.1 and [L4].

step 3.1step 1.1L3L4

5.1

The Cantor normal form of $ω^{4}$ is $ω^{4} \cdot 1$ : the largest $β$ with $ω^{β} \leq ω^{4}$ is $4$ , because $β \mapsto ω^{β}$ is strictly increasing by [L4] and $4 < β$ would give $ω^{4} < ω^{β}$ ; dividing by $ω^{4} > 0$ as in [L5] gives $ω^{4} = ω^{4} \cdot 1 + 0$ with remainder $0 < ω^{4}$ , so the datum of length $1$ with exponent $4$ and coefficient $1$ has value $ω^{4}$ , and it is the only normal form by the uniqueness in [L5].

step 4.1L1L2L4L5

6.1

So $(ω^{2} + ω \cdot 3 + 5) \cdot ω^{2} = ω^{4}$ , with Cantor normal form $ω^{4} \cdot 1$ , while $(ω^{2} + ω \cdot 3 + 5) + (ω \cdot 2 + 7) = ω^{2} + ω \cdot 5 + 7$ .

step 5.1step 4.1step 2.2∎

Remarks

Why the tail vanishes under multiplication on the right. The squeeze in step 3.1 is the whole mechanism: $α$ is trapped between $ω^{2}$ and $ω^{2} \cdot 2$ , and multiplying either bound on the right by $ω$ gives $ω^{3}$ , because $ω^{2} \cdot 2 \cdot n = ω^{2} \cdot (2 n)$ runs through the same cofinal family as $ω^{2} \cdot n$ . Anything of the form "leading term plus smaller stuff" therefore behaves, under multiplication by a limit on the right, exactly like its leading term.

Why the tail does not vanish under addition. In step 2.2 the lower part of the left summand, here $5$ , is absorbed by the leading term of the right summand, but the term $ω^{2}$ of the left summand survives, and the two coefficients of $ω^{1}$ add. The general rule is the same computation: adding on the left of $ω^{β}$ anything smaller than $ω^{β}$ changes nothing, which is the additive indecomposability used inside the proof of Cantor normal form: every nonzero ordinal is $ω^{β_{0}} \cdot c_{0} + \dots + ω^{β_{k - 1}} \cdot c_{k - 1}$ with $β_{0} > \dots > β_{k - 1}$ and each $c_{i}$ a nonzero natural number, in exactly one way.

A check on the answer. $ω^{4}$ has Cantor normal form of length $1$ , so $α \cdot ω^{2}$ is a power of $ω$ ; that is consistent with the previous remark, since $α$ has leading term $ω^{2} \cdot 1$ and $ω^{2} \cdot ω^{2} = ω^{4}$ by the sum law in [L4].

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

45 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)
T. Jech, Set Theory, 3rd millennium ed., Ch. 2 (Ordinal numbers) (standard reference, not scraped)
A. Marks, Set Theory (standard reference, not scraped)

The Cantor normal form of (ω2+ω⋅3+5)⋅ω2(ω2+ω⋅3+5)⋅ω2, computed by the division algorithm