Principal ordinals

If op is a binary operation on ordinals, we say that an ordinal o is op-principal (or op-indecomposable) whenever a < o and b < o imply op a b < o. Most commonly, one talks of additive and multiplicative principal ordinals.

Additive principal ordinals were originally called "gamma numbers" by Cantor, but this term now more commonly refers to the values given by Ordinal.gamma. Likewise, multiplicative principal ordinals are sometimes known as "delta numbers". Exponential principal ordinals are (barring edge cases) equivalent to the epsilon numbers given by Ordinal.epsilon.

Main definitions and results

• IsPrincipal: A principal (or indecomposable) ordinal under some binary operation. We include 0 and other typically excluded edge cases for simplicity.
• not_bddAbove_setOfPred_isPrincipal: Principal ordinals (under any operation) are unbounded.
• isPrincipal_add_iff_zero_or_omega0_opow: The additive principal ordinals are 0 and the ordinal powers of ω.
• isPrincipal_mul_iff_le_two_or_omega0_opow_opow: The multiplicative principal ordinals are 0, 1, 2, and the ordinals ω ^ ω ^ x.

TODO

• Prove that the exponential principal ordinals are 0, 1, 2, ω, or ε_ x.

Tags

additively indecomposable, multiplicatively indecomposable

Principal ordinals under an arbitrary operation

def Ordinal.IsPrincipal (op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}) (o : Ordinal.{u_1}) : Prop

An ordinal o is said to be principal (or indecomposable) under an operation when Iio o is closed under that operation.

For simplicity, we break usual convention and regard 0 as principal.

Equations

• Ordinal.IsPrincipal op o = ∀ ⦃a b : Ordinal.{?u.1}⦄, a < o → b < o → op a b < o

theorem Ordinal.isPrincipal_swap_iff {o : Ordinal.{u}} {op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}} : IsPrincipal (Function.swap op) o ↔ IsPrincipal op o

theorem Ordinal.not_isPrincipal_iff {o : Ordinal.{u}} {op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}} : ¬IsPrincipal op o ↔ ∃ a < o, ∃ b < o, o ≤ op a b

theorem Ordinal.isPrincipal_iff_of_monotone {o : Ordinal.{u}} {op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}} (h₁ : ∀ (a : Ordinal.{u}), Monotone (op a)) (h₂ : ∀ (a : Ordinal.{u}), Monotone (Function.swap op a)) : IsPrincipal op o ↔ ∀ a < o, op a a < o

theorem Ordinal.not_isPrincipal_iff_of_monotone {o : Ordinal.{u}} {op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}} (h₁ : ∀ (a : Ordinal.{u}), Monotone (op a)) (h₂ : ∀ (a : Ordinal.{u}), Monotone (Function.swap op a)) : ¬IsPrincipal op o ↔ ∃ a < o, o ≤ op a a

@[simp]

theorem Ordinal.isPrincipal_zero {op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}} : IsPrincipal op 0

@[simp]

theorem Ordinal.isPrincipal_one_iff {op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}} : IsPrincipal op 1 ↔ op 0 0 = 0

theorem Ordinal.IsPrincipal.iterate_lt {a o : Ordinal.{u}} {op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}} (hao : a < o) (ho : IsPrincipal op o) (n : ℕ) : (op a)^[n] a < o

theorem Ordinal.op_eq_self_of_isPrincipal {a o : Ordinal.{u}} {op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}} (hao : a < o) (H : Order.IsNormal (op a)) (ho : IsPrincipal op o) (ho' : Order.IsSuccLimit o) : op a o = o

theorem Ordinal.nfp_le_of_isPrincipal {a o : Ordinal.{u}} {op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}} (hao : a < o) (ho : IsPrincipal op o) : nfp (op a) a ≤ o

theorem Ordinal.IsPrincipal.sSup {op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}} {s : Set Ordinal.{u_1}} (H : ∀ x ∈ s, IsPrincipal op x) : IsPrincipal op (sSup s)

theorem Ordinal.IsPrincipal.iSup {op : Ordinal.{u_2} → Ordinal.{u_2} → Ordinal.{u_2}} {ι : Sort u_1} {f : ι → Ordinal.{u_2}} (H : ∀ (i : ι), IsPrincipal op (f i)) : IsPrincipal op (⨆ (i : ι), f i)

theorem Ordinal.not_bddAbove_setOfPred_isPrincipal (op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}) : ¬BddAbove {o : Ordinal.{u_1} | IsPrincipal op o}

Principal ordinals under any operation are unbounded.

@[deprecated Ordinal.not_bddAbove_setOfPred_isPrincipal (since := "2026-07-09")]

theorem Ordinal.not_bddAbove_setOf_isPrincipal (op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}) : ¬BddAbove {o : Ordinal.{u_1} | IsPrincipal op o}

Alias of Ordinal.not_bddAbove_setOfPred_isPrincipal.

---

Principal ordinals under any operation are unbounded.

Additive principal ordinals

theorem Ordinal.isPrincipal_add_iff_add_self_lt {a : Ordinal.{u}} : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 + x2) a ↔ ∀ b < a, b + b < a

theorem Ordinal.IsPrincipal.mul_natCast_lt {a o : Ordinal.{u}} (ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 + x2) o) (ha : a < o) (n : ℕ) : a * ↑n < o

theorem Ordinal.isPrincipal_add_one : IsPrincipal (fun (x1 x2 : Ordinal.{u_1}) => x1 + x2) 1

theorem Ordinal.isPrincipal_add_of_le_one {o : Ordinal.{u}} (ho : o ≤ 1) : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 + x2) o

theorem Ordinal.isSuccLimit_of_isPrincipal_add {o : Ordinal.{u}} (ho₁ : 1 < o) (ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 + x2) o) : Order.IsSuccLimit o

theorem Ordinal.isPrincipal_add_iff_add_left_eq_self {o : Ordinal.{u}} : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 + x2) o ↔ ∀ a < o, a + o = o

theorem Ordinal.IsPrincipal.add_eq_right {a o : Ordinal.{u}} (ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 + x2) o) (ha : a < o) : a + o = o

theorem Ordinal.IsPrincipal.add_eq_right_of_le {a b c : Ordinal.{u}} (hb : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 + x2) b) (hab : a < b) (hbc : b ≤ c) : a + c = c

theorem Ordinal.exists_lt_add_of_not_isPrincipal_add {a : Ordinal.{u}} (ha : ¬IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 + x2) a) : ∃ b < a, ∃ c < a, b + c = a

theorem Ordinal.isPrincipal_add_iff_add_lt_ne_self {a : Ordinal.{u}} : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 + x2) a ↔ ∀ b < a, ∀ c < a, b + c ≠ a

theorem Ordinal.isPrincipal_add_omega0 : IsPrincipal (fun (x1 x2 : Ordinal.{u_1}) => x1 + x2) omega0

theorem Ordinal.add_of_omega0_le {a b : Ordinal.{u}} : a < omega0 → omega0 ≤ b → a + b = b

theorem Ordinal.isPrincipal_add_omega0_opow (o : Ordinal.{u_1}) : IsPrincipal (fun (x1 x2 : Ordinal.{u_1}) => x1 + x2) (omega0 ^ o)

theorem Ordinal.add_omega0_opow {a b : Ordinal.{u}} (h : a < omega0 ^ b) : a + omega0 ^ b = omega0 ^ b

theorem Ordinal.add_of_omega0_opow_le {a b c : Ordinal.{u}} (h₁ : a < omega0 ^ b) (h₂ : omega0 ^ b ≤ c) : a + c = c

theorem Ordinal.isLeast_sub_lt_omega0_opow_log {a : Ordinal.{u}} (h : a ≠ 0) : IsLeast {b : Ordinal.{u} | a - b < a} (omega0 ^ log omega0 a)

For a ≠ 0, the largest power of ω which is less or equal to it is also the smallest ordinal b with a - b < a.

theorem Ordinal.isPrincipal_add_iff_zero_or_omega0_opow {o : Ordinal.{u}} : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 + x2) o ↔ o = 0 ∨ o ∈ Set.range fun (x : Ordinal.{u}) => omega0 ^ x

The main characterization theorem for additive principal ordinals.

theorem Ordinal.isPrincipal_add_opow_of_isPrincipal_add {a : Ordinal.{u_1}} (ha : IsPrincipal (fun (x1 x2 : Ordinal.{u_1}) => x1 + x2) a) (b : Ordinal.{u_1}) : IsPrincipal (fun (x1 x2 : Ordinal.{u_1}) => x1 + x2) (a ^ b)

theorem Ordinal.isPrincipal_add_mul_of_isPrincipal_add (a : Ordinal.{u}) {b : Ordinal.{u}} (hb₁ : b ≠ 1) (hb : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 + x2) b) : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 + x2) (a * b)

Multiplicative principal ordinals

theorem Ordinal.isPrincipal_mul_one : IsPrincipal (fun (x1 x2 : Ordinal.{u_1}) => x1 * x2) 1

theorem Ordinal.isPrincipal_mul_two : IsPrincipal (fun (x1 x2 : Ordinal.{u_1}) => x1 * x2) 2

theorem Ordinal.isPrincipal_mul_of_le_two {o : Ordinal.{u}} (ho : o ≤ 2) : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 * x2) o

theorem Ordinal.isPrincipal_add_of_isPrincipal_mul {o : Ordinal.{u}} (ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 * x2) o) (ho₂ : o ≠ 2) : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 + x2) o

theorem Ordinal.isSuccLimit_of_isPrincipal_mul {o : Ordinal.{u}} (ho₂ : 2 < o) (ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 * x2) o) : Order.IsSuccLimit o

theorem Ordinal.isPrincipal_mul_iff_mul_left_eq {o : Ordinal.{u}} : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 * x2) o ↔ ∀ (a : Ordinal.{u}), 0 < a → a < o → a * o = o

theorem Ordinal.isPrincipal_mul_omega0 : IsPrincipal (fun (x1 x2 : Ordinal.{u_1}) => x1 * x2) omega0

theorem Ordinal.mul_omega0 {a : Ordinal.{u}} (a0 : 0 < a) (ha : a < omega0) : a * omega0 = omega0

theorem Ordinal.natCast_mul_omega0 {n : ℕ} (hn : 0 < n) : ↑n * omega0 = omega0

theorem Ordinal.mul_lt_omega0_opow {a b c : Ordinal.{u}} (c0 : 0 < c) (ha : a < omega0 ^ c) (hb : b < omega0) : a * b < omega0 ^ c

theorem Ordinal.mul_omega0_opow_opow {a b : Ordinal.{u}} (a0 : 0 < a) (h : a < omega0 ^ omega0 ^ b) : a * omega0 ^ omega0 ^ b = omega0 ^ omega0 ^ b

theorem Ordinal.isPrincipal_mul_omega0_opow_opow (o : Ordinal.{u_1}) : IsPrincipal (fun (x1 x2 : Ordinal.{u_1}) => x1 * x2) (omega0 ^ omega0 ^ o)

theorem Ordinal.isPrincipal_add_of_isPrincipal_mul_opow {b o : Ordinal.{u}} (hb : 1 < b) (ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 * x2) (b ^ o)) : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 + x2) o

theorem Ordinal.isPrincipal_mul_iff_le_two_or_omega0_opow_opow {o : Ordinal.{u}} : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 * x2) o ↔ o ≤ 2 ∨ o ∈ Set.range fun (x : Ordinal.{u}) => omega0 ^ omega0 ^ x

The main characterization theorem for multiplicative principal ordinals.

theorem Ordinal.mul_omega0_dvd {a : Ordinal.{u}} (a0 : 0 < a) (ha : a < omega0) {b : Ordinal.{u}} : omega0 ∣ b → a * b = b

theorem Ordinal.mul_eq_opow_log_succ {a b : Ordinal.{u}} (ha : a ≠ 0) (hb : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 * x2) b) (hb₂ : 2 < b) : a * b = b ^ Order.succ (log b a)

Exponential principal ordinals

theorem Ordinal.isPrincipal_opow_omega0 : IsPrincipal (fun (x1 x2 : Ordinal.{u_1}) => x1 ^ x2) omega0

theorem Ordinal.opow_omega0 {a : Ordinal.{u}} (a1 : 1 < a) (h : a < omega0) : a ^ omega0 = omega0

theorem Ordinal.natCast_opow_omega0 {n : ℕ} (hn : 1 < n) : ↑n ^ omega0 = omega0