Cantor Normal Form

The Cantor normal form of an ordinal is generally defined as its base ω expansion, with its non-zero exponents in decreasing order. Here, we more generally define a base b expansion Ordinal.CNF in this manner, which is well-behaved for any b ≥ 2.

Implementation notes

We implement Ordinal.CNF as an association list, where keys are exponents and values are coefficients. This is because this structure intrinsically reflects two key properties of the Cantor normal form:

• It is ordered.
• It has finitely many entries.

Todo

• Prove the basic results relating the CNF to the arithmetic operations on ordinals.

Cantor normal form as a list

@[irreducible]

def Ordinal.CNF.rec (b : Ordinal.{u_2}) {C : Ordinal.{u_2} → Sort u_1} (H0 : C 0) (H : (o : Ordinal.{u_2}) → o ≠ 0 → C (o % b ^ log b o) → C o) (o : Ordinal.{u_2}) : C o

Inducts on the base b expansion of an ordinal.

Equations

• Ordinal.CNF.rec b H0 H o = if h : o = 0 then ⋯ ▸ H0 else H o h (Ordinal.CNF.rec b H0 H (o % b ^ Ordinal.log b o))

@[deprecated Ordinal.CNF.rec (since := "2025-08-18")]

def Ordinal.CNFRec (b : Ordinal.{u_2}) {C : Ordinal.{u_2} → Sort u_1} (H0 : C 0) (H : (o : Ordinal.{u_2}) → o ≠ 0 → C (o % b ^ log b o) → C o) (o : Ordinal.{u_2}) : C o

Alias of Ordinal.CNF.rec.

---

Inducts on the base b expansion of an ordinal.

Equations

• Ordinal.CNFRec = Ordinal.CNF.rec

@[simp]

theorem Ordinal.CNF.rec_zero {C : Ordinal.{u_2} → Sort u_1} (b : Ordinal.{u_2}) (H0 : C 0) (H : (o : Ordinal.{u_2}) → o ≠ 0 → C (o % b ^ log b o) → C o) : CNF.rec b H0 H 0 = H0

@[deprecated Ordinal.CNF.rec_zero (since := "2025-08-18")]

theorem Ordinal.CNFRec_zero {C : Ordinal.{u_2} → Sort u_1} (b : Ordinal.{u_2}) (H0 : C 0) (H : (o : Ordinal.{u_2}) → o ≠ 0 → C (o % b ^ log b o) → C o) : CNF.rec b H0 H 0 = H0

Alias of Ordinal.CNF.rec_zero.

theorem Ordinal.CNF.rec_pos (b : Ordinal.{u_2}) {o : Ordinal.{u_2}} {C : Ordinal.{u_2} → Sort u_1} (ho : o ≠ 0) (H0 : C 0) (H : (o : Ordinal.{u_2}) → o ≠ 0 → C (o % b ^ log b o) → C o) : CNF.rec b H0 H o = H o ho (CNF.rec b H0 H (o % b ^ log b o))

@[deprecated Ordinal.CNF.rec_pos (since := "2025-08-18")]

theorem Ordinal.CNFRec_pos (b : Ordinal.{u_2}) {o : Ordinal.{u_2}} {C : Ordinal.{u_2} → Sort u_1} (ho : o ≠ 0) (H0 : C 0) (H : (o : Ordinal.{u_2}) → o ≠ 0 → C (o % b ^ log b o) → C o) : CNF.rec b H0 H o = H o ho (CNF.rec b H0 H (o % b ^ log b o))

Alias of Ordinal.CNF.rec_pos.

noncomputable def Ordinal.CNF (b o : Ordinal.{u_1}) : List (Ordinal.{u_1} × Ordinal.{u_1})

The Cantor normal form of an ordinal o is the list of coefficients and exponents in the base-b expansion of o.

We special-case CNF 0 o = CNF 1 o = [(0, o)] for o ≠ 0.

CNF b (b ^ u₁ * v₁ + b ^ u₂ * v₂) = [(u₁, v₁), (u₂, v₂)]

Equations

• Ordinal.CNF b o = Ordinal.CNF.rec b [] (fun (o : Ordinal.{?u.15}) (x : o ≠ 0) (IH : List (Ordinal.{?u.15} × Ordinal.{?u.15})) => (Ordinal.log b o, o / b ^ Ordinal.log b o) :: IH) o

@[simp]

theorem Ordinal.CNF.zero_right (b : Ordinal.{u_1}) : CNF b 0 = []

@[deprecated Ordinal.CNF.zero_right (since := "2025-08-18")]

theorem Ordinal.CNF_zero (b : Ordinal.{u_1}) : CNF b 0 = []

Alias of Ordinal.CNF.zero_right.

theorem Ordinal.CNF.ne_zero {b o : Ordinal.{u_1}} (ho : o ≠ 0) : CNF b o = (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o)

Recursive definition for the Cantor normal form.

@[deprecated Ordinal.CNF.ne_zero (since := "2025-08-18")]

theorem Ordinal.CNF_ne_zero {b o : Ordinal.{u_1}} (ho : o ≠ 0) : CNF b o = (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o)

Alias of Ordinal.CNF.ne_zero.

---

Recursive definition for the Cantor normal form.

theorem Ordinal.CNF.opow_mul_add {b e x y : Ordinal.{u_1}} (hb : 1 < b) (hx : x ≠ 0) (hxb : x < b) (hy : y < b ^ e) : CNF b (b ^ e * x + y) = (e, x) :: CNF b y

theorem Ordinal.CNF.zero_left {o : Ordinal.{u_1}} (ho : o ≠ 0) : CNF 0 o = [(0, o)]

@[deprecated Ordinal.CNF.zero_left (since := "2025-08-18")]

theorem Ordinal.zero_CNF {o : Ordinal.{u_1}} (ho : o ≠ 0) : CNF 0 o = [(0, o)]

Alias of Ordinal.CNF.zero_left.

theorem Ordinal.CNF.one_left {o : Ordinal.{u_1}} (ho : o ≠ 0) : CNF 1 o = [(0, o)]

@[deprecated Ordinal.CNF.one_left (since := "2025-08-18")]

theorem Ordinal.one_CNF {o : Ordinal.{u_1}} (ho : o ≠ 0) : CNF 1 o = [(0, o)]

Alias of Ordinal.CNF.one_left.

theorem Ordinal.CNF.of_le_one {b o : Ordinal.{u_1}} (hb : b ≤ 1) (ho : o ≠ 0) : CNF b o = [(0, o)]

@[deprecated Ordinal.CNF.of_le_one (since := "2025-08-18")]

theorem Ordinal.CNF_of_le_one {b o : Ordinal.{u_1}} (hb : b ≤ 1) (ho : o ≠ 0) : CNF b o = [(0, o)]

Alias of Ordinal.CNF.of_le_one.

theorem Ordinal.CNF.of_lt {b o : Ordinal.{u_1}} (ho : o ≠ 0) (hb : o < b) : CNF b o = [(0, o)]

@[deprecated Ordinal.CNF.of_lt (since := "2025-08-18")]

theorem Ordinal.CNF_of_lt {b o : Ordinal.{u_1}} (ho : o ≠ 0) (hb : o < b) : CNF b o = [(0, o)]

Alias of Ordinal.CNF.of_lt.

theorem Ordinal.CNF.foldr (b o : Ordinal.{u_1}) : List.foldr (fun (p : Ordinal.{u_1} × Ordinal.{u_1}) (r : Ordinal.{u_1}) => b ^ p.1 * p.2 + r) 0 (CNF b o) = o

Evaluating the Cantor normal form of an ordinal returns the ordinal.

@[deprecated Ordinal.CNF.foldr (since := "2025-08-18")]

theorem Ordinal.CNF_foldr (b o : Ordinal.{u_1}) : List.foldr (fun (p : Ordinal.{u_1} × Ordinal.{u_1}) (r : Ordinal.{u_1}) => b ^ p.1 * p.2 + r) 0 (CNF b o) = o

Alias of Ordinal.CNF.foldr.

---

Evaluating the Cantor normal form of an ordinal returns the ordinal.

theorem Ordinal.CNF.fst_le_log {b o : Ordinal.{u}} {x : Ordinal.{u} × Ordinal.{u}} : x ∈ CNF b o → x.1 ≤ log b o

Every exponent in the Cantor normal form CNF b o is less or equal to log b o.

@[deprecated Ordinal.CNF.fst_le_log (since := "2025-08-18")]

theorem Ordinal.CNF_fst_le_log {b o : Ordinal.{u}} {x : Ordinal.{u} × Ordinal.{u}} : x ∈ CNF b o → x.1 ≤ log b o

Alias of Ordinal.CNF.fst_le_log.

---

Every exponent in the Cantor normal form CNF b o is less or equal to log b o.

theorem Ordinal.CNF.snd_pos {b o : Ordinal.{u}} {x : Ordinal.{u} × Ordinal.{u}} : x ∈ CNF b o → 0 < x.2

Every coefficient in a Cantor normal form is positive.

@[deprecated Ordinal.CNF.snd_pos (since := "2026-01-11")]

theorem Ordinal.CNF.lt_snd {b o : Ordinal.{u}} {x : Ordinal.{u} × Ordinal.{u}} : x ∈ CNF b o → 0 < x.2

Alias of Ordinal.CNF.snd_pos.

---

Every coefficient in a Cantor normal form is positive.

@[deprecated Ordinal.CNF.snd_pos (since := "2025-08-18")]

theorem Ordinal.CNF_lt_snd {b o : Ordinal.{u}} {x : Ordinal.{u} × Ordinal.{u}} : x ∈ CNF b o → 0 < x.2

Alias of Ordinal.CNF.snd_pos.

---

Every coefficient in a Cantor normal form is positive.

theorem Ordinal.CNF.snd_lt {b o : Ordinal.{u}} (hb : 1 < b) {x : Ordinal.{u} × Ordinal.{u}} : x ∈ CNF b o → x.2 < b

Every coefficient in the Cantor normal form CNF b o is less than b.

@[deprecated Ordinal.CNF.snd_lt (since := "2025-08-18")]

theorem Ordinal.CNF_snd_lt {b o : Ordinal.{u}} (hb : 1 < b) {x : Ordinal.{u} × Ordinal.{u}} : x ∈ CNF b o → x.2 < b

Alias of Ordinal.CNF.snd_lt.

---

Every coefficient in the Cantor normal form CNF b o is less than b.

theorem Ordinal.CNF.sortedGT (b o : Ordinal.{u_1}) : (List.map Prod.fst (CNF b o)).SortedGT

The exponents of the Cantor normal form are decreasing.

@[deprecated Ordinal.CNF.sortedGT (since := "2026-01-11")]

theorem Ordinal.CNF.sorted (b o : Ordinal.{u_1}) : (List.map Prod.fst (CNF b o)).SortedGT

Alias of Ordinal.CNF.sortedGT.

---

The exponents of the Cantor normal form are decreasing.

@[deprecated Ordinal.CNF.sortedGT (since := "2025-08-18")]

theorem Ordinal.CNF_sorted (b o : Ordinal.{u_1}) : (List.map Prod.fst (CNF b o)).SortedGT

Alias of Ordinal.CNF.sortedGT.

---

The exponents of the Cantor normal form are decreasing.

Cantor normal form as a finsupp

noncomputable def Ordinal.CNF.coeff (b o : Ordinal.{u_1}) : Ordinal.{u_1} →₀ Ordinal.{u_1}

CNF.coeff b o is the finitely supported function returning the coefficient of b ^ e in the Cantor Normal Form (CNF) of o, for each e.

Equations

• Ordinal.CNF.coeff b o = { entries := List.map Prod.toSigma (Ordinal.CNF b o), nodupKeys := ⋯ }.lookupFinsupp

theorem Ordinal.CNF.support_coeff (b o : Ordinal.{u_1}) : (coeff b o).support = (List.map Prod.fst (CNF b o)).toFinset

theorem Ordinal.CNF.coeff_of_mem_CNF {b o e c : Ordinal.{u_1}} (h : (e, c) ∈ CNF b o) : (coeff b o) e = c

theorem Ordinal.CNF.coeff_of_notMem_CNF {b o e : Ordinal.{u_1}} (h : e ∉ List.map Prod.fst (CNF b o)) : (coeff b o) e = 0

@[deprecated Ordinal.CNF.coeff_of_notMem_CNF (since := "2026-01-11")]

theorem Ordinal.CNF.coeff_of_not_mem_CNF {b o e : Ordinal.{u_1}} (h : e ∉ List.map Prod.fst (CNF b o)) : (coeff b o) e = 0

Alias of Ordinal.CNF.coeff_of_notMem_CNF.

theorem Ordinal.CNF.coeff_eq_zero_of_lt {b o e : Ordinal.{u_1}} (h : o < b ^ e) : (coeff b o) e = 0

theorem Ordinal.CNF.coeff_zero_apply (b e : Ordinal.{u_1}) : (coeff b 0) e = 0

@[simp]

theorem Ordinal.CNF.coeff_zero_right (b : Ordinal.{u_1}) : coeff b 0 = 0

theorem Ordinal.CNF.coeff_of_le_one {b : Ordinal.{u_1}} (hb : b ≤ 1) (o : Ordinal.{u_1}) : coeff b o = Finsupp.single 0 o

@[simp]

theorem Ordinal.CNF.coeff_zero_left (o : Ordinal.{u_1}) : coeff 0 o = Finsupp.single 0 o

@[simp]

theorem Ordinal.CNF.coeff_one_left (o : Ordinal.{u_1}) : coeff 1 o = Finsupp.single 0 o

theorem Ordinal.CNF.coeff_opow_mul_add {b e x y : Ordinal.{u_1}} (hb : 1 < b) (hx : x ≠ 0) (hxb : x < b) (hy : y < b ^ e) : coeff b (b ^ e * x + y) = Finsupp.single e x + coeff b y

Evaluate a Cantor normal form

noncomputable def Ordinal.CNF.eval (b : Ordinal.{u_1}) (f : Ordinal.{u_1} →₀ Ordinal.{u_1}) : Ordinal.{u_1}

CNF.eval f evaluates a Finsupp f : Ordinal →₀ Ordinal, interpreted as a base b expansion on ordinals.

Equations

• Ordinal.CNF.eval b f = List.foldr (fun (p r : Ordinal.{?u.18}) => b ^ p * f p + r) 0 (f.support.sort fun (x1 x2 : Ordinal.{?u.18}) => x1 ≥ x2)

@[simp]

theorem Ordinal.CNF.eval_zero_right (b : Ordinal.{u_1}) : eval b 0 = 0

theorem Ordinal.CNF.eval_single_add' (b : Ordinal.{u_1}) {e x : Ordinal.{u_1}} {f : Ordinal.{u_1} →₀ Ordinal.{u_1}} (h : ∀ e' ∈ f.support, e' < e) : eval b (Finsupp.single e x + f) = b ^ e * x + eval b f

For a slightly stronger version, see eval_single_add.

@[simp]

theorem Ordinal.CNF.eval_single (b e x : Ordinal.{u_1}) : eval b (Finsupp.single e x) = b ^ e * x

theorem Ordinal.CNF.eval_single_add (b : Ordinal.{u_1}) {e x : Ordinal.{u_1}} {f : Ordinal.{u_1} →₀ Ordinal.{u_1}} (h : ∀ e' ∈ f.support, e' ≤ e) : eval b (Finsupp.single e x + f) = b ^ e * x + eval b f

theorem Ordinal.CNF.eval_add (b : Ordinal.{u_1}) {f₁ f₂ : Ordinal.{u_1} →₀ Ordinal.{u_1}} (h : ∀ e₁ ∈ f₁.support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁) : eval b (f₁ + f₂) = eval b f₁ + eval b f₂

theorem Ordinal.CNF.eval_lt {b e : Ordinal.{u_1}} {f : Ordinal.{u_1} →₀ Ordinal.{u_1}} (hb : ∀ (e' : Ordinal.{u_1}), f e' < b) (he : ∀ e' ∈ f.support, e' < e) : eval b f < b ^ e

@[simp]

theorem Ordinal.CNF.eval_coeff (b o : Ordinal.{u_1}) : eval b (coeff b o) = o

theorem Ordinal.CNF.coeff_eval {b : Ordinal.{u_1}} (hb : 1 < b) {f : Ordinal.{u_1} →₀ Ordinal.{u_1}} (hf : ∀ (e : Ordinal.{u_1}), f e < b) : coeff b (eval b f) = f

theorem Ordinal.CNF.coeff_injective (b : Ordinal.{u_1}) : Function.Injective (coeff b)

@[simp]

theorem Ordinal.CNF.coeff_inj {b x y : Ordinal.{u_1}} : coeff b x = coeff b y ↔ x = y