Alphabeta Math
ExampleConstruction: AI-adaptedVerification: AI-generatedSession-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.

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

Example

Put α=ω2+ω⋅3+5\alpha = \omega^{2} + \omega \cdot 3 + 5, which is already in Cantor normal form (Cantor normal form: every nonzero ordinal is ωβ0⋅c0+⋯+ωβk−1⋅ck−1\omega^{\beta_0}\cdot c_0 + \cdots + \omega^{\beta_{k-1}}\cdot c_{k-1} with β0>⋯>βk−1\beta_0 > \cdots > \beta_{k-1} and each cic_i a nonzero natural number, in exactly one way): the exponents 2>1>02 > 1 > 0 strictly decrease and the coefficients 1,3,51, 3, 5 are nonzero natural numbers, since ω⋅3=ω1⋅3\omega \cdot 3 = \omega^{1} \cdot 3 and 5=ω0⋅55 = \omega^{0} \cdot 5. Then

α⋅ω2=ω4,\alpha \cdot \omega^{2} = \omega^{4},

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

Addition behaves quite differently. Also computed below:

(ω2+ω⋅3+5)+(ω⋅2+7)=ω2+ω⋅5+7,\big(\omega^{2} + \omega \cdot 3 + 5\big) + \big(\omega \cdot 2 + 7\big) = \omega^{2} + \omega \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+ω⋅3+5\alpha = \omega^{2} + \omega \cdot 3 + 5, with the operations of Ordinal addition α+β\alpha + \beta, Ordinal multiplication α⋅β\alpha \cdot \beta and Ordinal exponentiation αβ\alpha^{\beta}, with the conventions α0=1\alpha^{0} = 1 and 00=10^{0} = 1; the finite ordinals 2,3,4,5,72, 3, 4, 5, 7 are elements of ω\omega (The natural numbers N\mathbb{N} (von Neumann), ω\omega is the least limit ordinal). Products bind tighter than sums, so ω⋅3+5\omega \cdot 3 + 5 is (ω⋅3)+5(\omega \cdot 3) + 5.

[L1]

α⋅δ+=α⋅δ+α\alpha \cdot \delta^{+} = \alpha \cdot \delta + \alpha and α⋅λ=sup⁡{α⋅ξ:ξ∈λ}\alpha \cdot \lambda = \sup\{\alpha \cdot \xi : \xi \in \lambda\} for limit λ\lambda (Ordinal multiplication α⋅β\alpha \cdot \beta); αδ+=αδ⋅α\alpha^{\delta^{+}} = \alpha^{\delta} \cdot \alpha and α0=1\alpha^{0} = 1 (Ordinal exponentiation αβ\alpha^{\beta}, with the conventions α0=1\alpha^{0} = 1 and 00=10^{0} = 1); μ+0=μ\mu + 0 = \mu, μ+δ+=(μ+δ)+\mu + \delta^{+} = (\mu + \delta)^{+} and μ+λ=sup⁡{μ+ξ:ξ∈λ}\mu + \lambda = \sup\{\mu + \xi : \xi \in \lambda\} for limit λ\lambda (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 and 0+μ=μ0 + \mu = \mu (claim (a)); ν<θ\nu < \theta implies μ+ν<μ+θ\mu + \nu < \mu + \theta (claim (b)); for μ>0\mu > 0, ν<θ\nu < \theta implies μν<μθ\mu\nu < \mu\theta (claim (d)); μ≤ν\mu \le \nu implies μγ≤νγ\mu\gamma \le \nu\gamma (claim (e)); μ+λ=sup⁡{μ+ξ:ξ∈λ}\mu + \lambda = \sup\{\mu + \xi : \xi \in \lambda\} and μ⋅λ=sup⁡{μη:η∈D}\mu \cdot \lambda = \sup\{\mu\eta : \eta \in D\} for μ>0\mu > 0, λ\lambda a limit and D⊆λD \subseteq \lambda nonempty with sup⁡D=λ\sup D = \lambda (claim (f)).

[L3]

⋅\cdot is associative and μ(ν+θ)=μν+μθ\mu(\nu + \theta) = \mu\nu + \mu\theta (Ordinal multiplication is associative, and α⋅(β+γ)=α⋅β+α⋅γ\alpha \cdot (\beta + \gamma) = \alpha\cdot\beta + \alpha\cdot\gamma); ++ is associative (Ordinal addition is associative).

[L4]

αβ+γ=αβ⋅αγ\alpha^{\beta + \gamma} = \alpha^{\beta} \cdot \alpha^{\gamma}, α1=α\alpha^{1} = \alpha, and for α>1\alpha > 1 the map β↦αβ\beta \mapsto \alpha^{\beta} is strictly increasing (αβ+γ=αβ⋅αγ\alpha^{\beta+\gamma} = \alpha^{\beta}\cdot\alpha^{\gamma} and (αβ)γ=αβ⋅γ(\alpha^{\beta})^{\gamma} = \alpha^{\beta\cdot\gamma}; and for α>1\alpha > 1 exponentiation is strictly increasing with β≤αβ\beta \le \alpha^{\beta}).

[L5]

For μ>0\mu > 0 every ν\nu is μ⋅ξ+ρ\mu \cdot \xi + \rho with ρ<μ\rho < \mu, uniquely (For α>0\alpha > 0 every ordinal β\beta is α⋅ξ+ρ\alpha \cdot \xi + \rho with ρ<α\rho < \alpha, in exactly one way); every nonzero ordinal has exactly one Cantor normal form (Cantor normal form: every nonzero ordinal is ωβ0⋅c0+⋯+ωβk−1⋅ck−1\omega^{\beta_0}\cdot c_0 + \cdots + \omega^{\beta_{k-1}}\cdot c_{k-1} with β0>⋯>βk−1\beta_0 > \cdots > \beta_{k-1} and each cic_i a nonzero natural number, in exactly one way).

[L6]

For m,n∈ωm, n \in \omega the ordinals m+nm + n and m⋅nm \cdot n lie in ω\omega and agree with the natural-number sum and product (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).

[L7]

ω\omega is a limit ordinal with ⋃ω=ω\bigcup \omega = \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 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=ω\omega^{1} = \omega and ω2=ω1+=ω1⋅ω=ω⋅ω\omega^{2} = \omega^{1^{+}} = \omega^{1} \cdot \omega = \omega \cdot \omega by [L1] and [L4]; ω⋅3+ω=ω⋅3+=ω⋅4\omega \cdot 3 + \omega = \omega \cdot 3^{+} = \omega \cdot 4, ω+ω=ω⋅1+ω=ω⋅1+=ω⋅2\omega + \omega = \omega \cdot 1 + \omega = \omega \cdot 1^{+} = \omega \cdot 2, and ω2+ω2=ω2⋅1+ω2=ω2⋅2\omega^{2} + \omega^{2} = \omega^{2} \cdot 1 + \omega^{2} = \omega^{2} \cdot 2 by [L1] and [L2].

L1L2L4
1.2

For n∈ωn \in \omega the ordinals 2⋅n2 \cdot n and 5+n5 + n lie in ω\omega by [L6], hence are subsets of ω\omega by [L7]; and n=1⋅n≤2⋅nn = 1 \cdot n \le 2 \cdot n and n≤5+nn \le 5 + n by [L2], so both {2⋅n:n∈ω}\{2 \cdot n : n \in \omega\} and {5+n:n∈ω}\{5 + n : n \in \omega\} are nonempty subsets of ω\omega with supremum ⋃ω=ω\bigcup \omega = \omega.

L2L6L7
2.1

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

step 1.1L1L2L7
2.2

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

step 1.2step 1.1L1L3L6
3.1

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

step 2.1step 1.2step 1.1L1L2L3L4
4.1

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

step 3.1step 1.1L3L4
5.1

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

step 4.1L1L2L4L5
6.1

So (ω2+ω⋅3+5)⋅ω2=ω4(\omega^{2} + \omega \cdot 3 + 5) \cdot \omega^{2} = \omega^{4}, with Cantor normal form ω4⋅1\omega^{4} \cdot 1, while (ω2+ω⋅3+5)+(ω⋅2+7)=ω2+ω⋅5+7(\omega^{2} + \omega \cdot 3 + 5) + (\omega \cdot 2 + 7) = \omega^{2} + \omega \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: α\alpha is trapped between ω2\omega^{2} and ω2⋅2\omega^{2} \cdot 2, and multiplying either bound on the right by ω\omega gives ω3\omega^{3}, because ω2⋅2⋅n=ω2⋅(2n)\omega^{2} \cdot 2 \cdot n = \omega^{2} \cdot (2n) runs through the same cofinal family as ω2⋅n\omega^{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 55, is absorbed by the leading term of the right summand, but the term ω2\omega^{2} of the left summand survives, and the two coefficients of ω1\omega^{1} add. The general rule is the same computation: adding on the left of ωβ\omega^{\beta} anything smaller than ωβ\omega^{\beta} changes nothing, which is the additive indecomposability used inside the proof of Cantor normal form: every nonzero ordinal is ωβ0⋅c0+⋯+ωβk−1⋅ck−1\omega^{\beta_0}\cdot c_0 + \cdots + \omega^{\beta_{k-1}}\cdot c_{k-1} with β0>⋯>βk−1\beta_0 > \cdots > \beta_{k-1} and each cic_i a nonzero natural number, in exactly one way.

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

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: 66 results over 30 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