Ordinal notation

Constructive ordinal arithmetic for ordinals below ε₀.

We define a type ONote, with constructors 0 : ONote and ONote.oadd e n a representing ω ^ e * n + a. We say that o is in Cantor normal form - ONote.NF o - if either o = 0 or o = ω ^ e * n + a with a < ω ^ e and a in Cantor normal form.

The type NONote is the type of ordinals below ε₀ in Cantor normal form. Various operations (addition, subtraction, multiplication, power function) are defined on ONote and NONote.

inductive ONote : Type

Recursive definition of an ordinal notation. zero denotes the ordinal 0, and oadd e n a is intended to refer to ω^e * n + a. For this to be valid Cantor normal form, we must have the exponents decrease to the right, but we can't state this condition until we've defined repr, so it is a separate definition NF.

• zero: ONote
• oadd: ONote → ℕ+ → ONote → ONote

instance instDecidableEqONote : DecidableEq ONote

Equations

• instDecidableEqONote = decEqONote✝

instance ONote.instZeroONote : Zero ONote

Notation for 0

Equations

• ONote.instZeroONote = { zero := ONote.zero }

@[simp]

theorem ONote.zero_def : ONote.zero = 0

instance ONote.instInhabitedONote : Inhabited ONote

Equations

• ONote.instInhabitedONote = { default := 0 }

instance ONote.instOneONote : One ONote

Notation for 1

Equations

• ONote.instOneONote = { one := ONote.oadd 0 1 0 }

def ONote.omega : ONote

Notation for ω

Equations

• ONote.omega = ONote.oadd 1 1 0

noncomputable def ONote.repr : ONote → Ordinal.{0}

The ordinal denoted by a notation

Equations

• ONote.repr ONote.zero = 0
• ONote.repr (ONote.oadd e n a) = Ordinal.omega ^ ONote.repr e * ↑↑n + ONote.repr a

def ONote.toStringAux1 (e : ONote) (n : ℕ) (s : String) : String

Auxiliary definition to print an ordinal notation

Equations

• ONote.toStringAux1 e n s = if e = 0 then toString n else (if e = 1 then "ω" else "ω^(" ++ s ++ ")") ++ if n = 1 then "" else "*" ++ toString n

def ONote.toString : ONote → String

Print an ordinal notation

Equations

• ONote.toString ONote.zero = "0"
• ONote.toString (ONote.oadd e n ONote.zero) = ONote.toStringAux1 e (↑n) (ONote.toString e)
• ONote.toString (ONote.oadd e n a) = ONote.toStringAux1 e (↑n) (ONote.toString e) ++ " + " ++ ONote.toString a

def ONote.repr' (prec : ℕ) : ONote → Lean.Format

Print an ordinal notation

Equations

• One or more equations did not get rendered due to their size.
• ONote.repr' prec ONote.zero = Std.Format.text "0"

instance ONote.instToStringONote : ToString ONote

Equations

• ONote.instToStringONote = { toString := ONote.toString }

instance ONote.instReprONote : Repr ONote

Equations

• ONote.instReprONote = { reprPrec := fun (o : ONote) (prec : ℕ) => ONote.repr' prec o }

instance ONote.instPreorderONote : Preorder ONote

Equations

• ONote.instPreorderONote = Preorder.mk ONote.instPreorderONote.proof_1 ONote.instPreorderONote.proof_2

theorem ONote.lt_def {x : ONote} {y : ONote} : x < y ↔ ONote.repr x < ONote.repr y

theorem ONote.le_def {x : ONote} {y : ONote} : x ≤ y ↔ ONote.repr x ≤ ONote.repr y

instance ONote.instWellFoundedRelationONote : WellFoundedRelation ONote

Equations

• ONote.instWellFoundedRelationONote = { rel := fun (x x_1 : ONote) => x < x_1, wf := ONote.instWellFoundedRelationONote.proof_1 }

def ONote.ofNat : ℕ → ONote

Convert a Nat into an ordinal

Equations

• ↑x = match x with | 0 => 0 | Nat.succ n => ONote.oadd 0 (Nat.succPNat n) 0

@[simp]

theorem ONote.ofNat_zero : ↑0 = 0

@[simp]

theorem ONote.ofNat_succ (n : ℕ) : ↑(Nat.succ n) = ONote.oadd 0 (Nat.succPNat n) 0

instance ONote.nat (n : ℕ) : OfNat ONote n

Equations

• ONote.nat n = { ofNat := ↑n }

@[simp]

theorem ONote.ofNat_one : ↑1 = 1

@[simp]

theorem ONote.repr_ofNat (n : ℕ) : ONote.repr ↑n = ↑n

theorem ONote.repr_one : ONote.repr ↑1 = ↑1

theorem ONote.omega_le_oadd (e : ONote) (n : ℕ+) (a : ONote) : Ordinal.omega ^ ONote.repr e ≤ ONote.repr (ONote.oadd e n a)

theorem ONote.oadd_pos (e : ONote) (n : ℕ+) (a : ONote) : 0 < ONote.oadd e n a

def ONote.cmp : ONote → ONote → Ordering

Compare ordinal notations

Equations

• ONote.cmp ONote.zero ONote.zero = Ordering.eq
• ONote.cmp x ONote.zero = Ordering.gt
• ONote.cmp ONote.zero x = Ordering.lt
• ONote.cmp (ONote.oadd e₁ n₁ a₁) (ONote.oadd e₂ n₂ a₂) = Ordering.orElse (ONote.cmp e₁ e₂) (Ordering.orElse (cmp ↑n₁ ↑n₂) (ONote.cmp a₁ a₂))

theorem ONote.eq_of_cmp_eq {o₁ : ONote} {o₂ : ONote} : ONote.cmp o₁ o₂ = Ordering.eq → o₁ = o₂

theorem ONote.zero_lt_one : 0 < 1

inductive ONote.NFBelow : ONote → Ordinal.{0} → Prop

NFBelow o b says that o is a normal form ordinal notation satisfying repr o < ω ^ b.

• zero: ∀ {b : Ordinal.{0}}, ONote.NFBelow 0 b
• oadd': ∀ {e : ONote} {n : ℕ+} {a : ONote} {eb b : Ordinal.{0}}, ONote.NFBelow e eb → ONote.NFBelow a (ONote.repr e) → ONote.repr e < b → ONote.NFBelow (ONote.oadd e n a) b

class ONote.NF (o : ONote) : Prop

A normal form ordinal notation has the form

ω ^ a₁ * n₁ + ω ^ a₂ * n₂ + ... ω ^ aₖ * nₖ where a₁ > a₂ > ... > aₖ and all the aᵢ are also in normal form.

We will essentially only be interested in normal form ordinal notations, but to avoid complicating the algorithms we define everything over general ordinal notations and only prove correctness with normal form as an invariant.

• out : Exists (ONote.NFBelow o)

instance ONote.NF.zero : ONote.NF 0

Equations

• ONote.NF.zero = (_ : ONote.NF 0)

theorem ONote.NFBelow.oadd {e : ONote} {n : ℕ+} {a : ONote} {b : Ordinal.{0}} : ONote.NF e → ONote.NFBelow a (ONote.repr e) → ONote.repr e < b → ONote.NFBelow (ONote.oadd e n a) b

theorem ONote.NFBelow.fst {e : ONote} {n : ℕ+} {a : ONote} {b : Ordinal.{0}} (h : ONote.NFBelow (ONote.oadd e n a) b) : ONote.NF e

theorem ONote.NF.fst {e : ONote} {n : ℕ+} {a : ONote} : ONote.NF (ONote.oadd e n a) → ONote.NF e

theorem ONote.NFBelow.snd {e : ONote} {n : ℕ+} {a : ONote} {b : Ordinal.{0}} (h : ONote.NFBelow (ONote.oadd e n a) b) : ONote.NFBelow a (ONote.repr e)

theorem ONote.NF.snd' {e : ONote} {n : ℕ+} {a : ONote} : ONote.NF (ONote.oadd e n a) → ONote.NFBelow a (ONote.repr e)

theorem ONote.NF.snd {e : ONote} {n : ℕ+} {a : ONote} (h : ONote.NF (ONote.oadd e n a)) : ONote.NF a

theorem ONote.NF.oadd {e : ONote} {a : ONote} (h₁ : ONote.NF e) (n : ℕ+) (h₂ : ONote.NFBelow a (ONote.repr e)) : ONote.NF (ONote.oadd e n a)

instance ONote.NF.oadd_zero (e : ONote) (n : ℕ+) [h : ONote.NF e] : ONote.NF (ONote.oadd e n 0)

Equations

• (_ : ONote.NF (ONote.oadd e n 0)) = (_ : ONote.NF (ONote.oadd e n 0))

theorem ONote.NFBelow.lt {e : ONote} {n : ℕ+} {a : ONote} {b : Ordinal.{0}} (h : ONote.NFBelow (ONote.oadd e n a) b) : ONote.repr e < b

theorem ONote.NFBelow_zero {o : ONote} : ONote.NFBelow o 0 ↔ o = 0

theorem ONote.NF.zero_of_zero {e : ONote} {n : ℕ+} {a : ONote} (h : ONote.NF (ONote.oadd e n a)) (e0 : e = 0) : a = 0

theorem ONote.NFBelow.repr_lt {o : ONote} {b : Ordinal.{0}} (h : ONote.NFBelow o b) : ONote.repr o < Ordinal.omega ^ b

theorem ONote.NFBelow.mono {o : ONote} {b₁ : Ordinal.{0}} {b₂ : Ordinal.{0}} (bb : b₁ ≤ b₂) (h : ONote.NFBelow o b₁) : ONote.NFBelow o b₂

theorem ONote.NF.below_of_lt {e : ONote} {n : ℕ+} {a : ONote} {b : Ordinal.{0}} (H : ONote.repr e < b) : ONote.NF (ONote.oadd e n a) → ONote.NFBelow (ONote.oadd e n a) b

theorem ONote.NF.below_of_lt' {o : ONote} {b : Ordinal.{0}} : ONote.repr o < Ordinal.omega ^ b → ONote.NF o → ONote.NFBelow o b

theorem ONote.nfBelow_ofNat (n : ℕ) : ONote.NFBelow (↑n) 1

instance ONote.nf_ofNat (n : ℕ) : ONote.NF ↑n

Equations

• (_ : ONote.NF ↑n) = (_ : ONote.NF ↑n)

instance ONote.nf_one : ONote.NF 1

Equations

• ONote.nf_one = (_ : ONote.NF 1)

theorem ONote.oadd_lt_oadd_1 {e₁ : ONote} {n₁ : ℕ+} {o₁ : ONote} {e₂ : ONote} {n₂ : ℕ+} {o₂ : ONote} (h₁ : ONote.NF (ONote.oadd e₁ n₁ o₁)) (h : e₁ < e₂) : ONote.oadd e₁ n₁ o₁ < ONote.oadd e₂ n₂ o₂

theorem ONote.oadd_lt_oadd_2 {e : ONote} {o₁ : ONote} {o₂ : ONote} {n₁ : ℕ+} {n₂ : ℕ+} (h₁ : ONote.NF (ONote.oadd e n₁ o₁)) (h : ↑n₁ < ↑n₂) : ONote.oadd e n₁ o₁ < ONote.oadd e n₂ o₂

theorem ONote.oadd_lt_oadd_3 {e : ONote} {n : ℕ+} {a₁ : ONote} {a₂ : ONote} (h : a₁ < a₂) : ONote.oadd e n a₁ < ONote.oadd e n a₂

theorem ONote.cmp_compares (a : ONote) (b : ONote) [ONote.NF a] [ONote.NF b] : Ordering.Compares (ONote.cmp a b) a b

theorem ONote.repr_inj {a : ONote} {b : ONote} [ONote.NF a] [ONote.NF b] : ONote.repr a = ONote.repr b ↔ a = b

theorem ONote.NF.of_dvd_omega_opow {b : Ordinal.{0}} {e : ONote} {n : ℕ+} {a : ONote} (h : ONote.NF (ONote.oadd e n a)) (d : Ordinal.omega ^ b ∣ ONote.repr (ONote.oadd e n a)) : b ≤ ONote.repr e ∧ Ordinal.omega ^ b ∣ ONote.repr a

theorem ONote.NF.of_dvd_omega {e : ONote} {n : ℕ+} {a : ONote} (h : ONote.NF (ONote.oadd e n a)) : Ordinal.omega ∣ ONote.repr (ONote.oadd e n a) → ONote.repr e ≠ 0 ∧ Ordinal.omega ∣ ONote.repr a

def ONote.TopBelow (b : ONote) : ONote → Prop

TopBelow b o asserts that the largest exponent in o, if it exists, is less than b. This is an auxiliary definition for decidability of NF.

Equations

• ONote.TopBelow b x = match x with | ONote.zero => True | ONote.oadd e a a_1 => ONote.cmp e b = Ordering.lt

instance ONote.decidableTopBelow : DecidableRel ONote.TopBelow

Equations

• One or more equations did not get rendered due to their size.

theorem ONote.nfBelow_iff_topBelow {b : ONote} [ONote.NF b] {o : ONote} : ONote.NFBelow o (ONote.repr b) ↔ ONote.NF o ∧ ONote.TopBelow b o

instance ONote.decidableNF : DecidablePred ONote.NF

Equations

• One or more equations did not get rendered due to their size.
• ONote.decidableNF ONote.zero = isTrue ONote.NF.zero

def ONote.addAux (e : ONote) (n : ℕ+) (o : ONote) : ONote

Auxiliary definition for add

Equations

• One or more equations did not get rendered due to their size.

def ONote.add : ONote → ONote → ONote

Addition of ordinal notations (correct only for normal input)

Equations

• ONote.add ONote.zero x = x
• ONote.add (ONote.oadd e n a) x = ONote.addAux e n (ONote.add a x)

instance ONote.instAddONote : Add ONote

Equations

• ONote.instAddONote = { add := ONote.add }

@[simp]

theorem ONote.zero_add (o : ONote) : 0 + o = o

theorem ONote.oadd_add (e : ONote) (n : ℕ+) (a : ONote) (o : ONote) : ONote.oadd e n a + o = ONote.addAux e n (a + o)

def ONote.sub : ONote → ONote → ONote

Subtraction of ordinal notations (correct only for normal input)

Equations

• One or more equations did not get rendered due to their size.
• ONote.sub ONote.zero x = 0
• ONote.sub x ONote.zero = x

instance ONote.instSubONote : Sub ONote

Equations

• ONote.instSubONote = { sub := ONote.sub }

theorem ONote.add_nfBelow {b : Ordinal.{0}} {o₁ : ONote} {o₂ : ONote} : ONote.NFBelow o₁ b → ONote.NFBelow o₂ b → ONote.NFBelow (o₁ + o₂) b

instance ONote.add_nf (o₁ : ONote) (o₂ : ONote) [ONote.NF o₁] [ONote.NF o₂] : ONote.NF (o₁ + o₂)

Equations

• (_ : ONote.NF (o₁ + o₂)) = (_ : ONote.NF (o₁ + o₂))

@[simp]

theorem ONote.repr_add (o₁ : ONote) (o₂ : ONote) [ONote.NF o₁] [ONote.NF o₂] : ONote.repr (o₁ + o₂) = ONote.repr o₁ + ONote.repr o₂

theorem ONote.sub_nfBelow {o₁ : ONote} {o₂ : ONote} {b : Ordinal.{0}} : ONote.NFBelow o₁ b → ONote.NF o₂ → ONote.NFBelow (o₁ - o₂) b

instance ONote.sub_nf (o₁ : ONote) (o₂ : ONote) [ONote.NF o₁] [ONote.NF o₂] : ONote.NF (o₁ - o₂)

Equations

• (_ : ONote.NF (o₁ - o₂)) = (_ : ONote.NF (o₁ - o₂))

@[simp]

theorem ONote.repr_sub (o₁ : ONote) (o₂ : ONote) [ONote.NF o₁] [ONote.NF o₂] : ONote.repr (o₁ - o₂) = ONote.repr o₁ - ONote.repr o₂

def ONote.mul : ONote → ONote → ONote

Multiplication of ordinal notations (correct only for normal input)

Equations

• ONote.mul ONote.zero x = 0
• ONote.mul x ONote.zero = 0
• ONote.mul (ONote.oadd e₁ n₁ a₁) (ONote.oadd e₂ n₂ a₂) = if e₂ = 0 then ONote.oadd e₁ (n₁ * n₂) a₁ else ONote.oadd (e₁ + e₂) n₂ (ONote.mul (ONote.oadd e₁ n₁ a₁) a₂)

instance ONote.instMulONote : Mul ONote

Equations

• ONote.instMulONote = { mul := ONote.mul }

instance ONote.instMulZeroClassONote : MulZeroClass ONote

Equations

• ONote.instMulZeroClassONote = MulZeroClass.mk ONote.instMulZeroClassONote.proof_1 ONote.instMulZeroClassONote.proof_2

theorem ONote.oadd_mul (e₁ : ONote) (n₁ : ℕ+) (a₁ : ONote) (e₂ : ONote) (n₂ : ℕ+) (a₂ : ONote) : ONote.oadd e₁ n₁ a₁ * ONote.oadd e₂ n₂ a₂ = if e₂ = 0 then ONote.oadd e₁ (n₁ * n₂) a₁ else ONote.oadd (e₁ + e₂) n₂ (ONote.oadd e₁ n₁ a₁ * a₂)

theorem ONote.oadd_mul_nfBelow {e₁ : ONote} {n₁ : ℕ+} {a₁ : ONote} {b₁ : Ordinal.{0}} (h₁ : ONote.NFBelow (ONote.oadd e₁ n₁ a₁) b₁) {o₂ : ONote} {b₂ : Ordinal.{0}} : ONote.NFBelow o₂ b₂ → ONote.NFBelow (ONote.oadd e₁ n₁ a₁ * o₂) (ONote.repr e₁ + b₂)

instance ONote.mul_nf (o₁ : ONote) (o₂ : ONote) [ONote.NF o₁] [ONote.NF o₂] : ONote.NF (o₁ * o₂)

Equations

• (_ : ONote.NF (x✝² * x✝¹)) = (_ : ONote.NF (x✝² * x✝¹))

@[simp]

theorem ONote.repr_mul (o₁ : ONote) (o₂ : ONote) [ONote.NF o₁] [ONote.NF o₂] : ONote.repr (o₁ * o₂) = ONote.repr o₁ * ONote.repr o₂

def ONote.split' : ONote → ONote × ℕ

Calculate division and remainder of o mod ω. split' o = (a, n) means o = ω * a + n.

Equations

• ONote.split' ONote.zero = (0, 0)
• ONote.split' (ONote.oadd e n a) = if e = 0 then (0, ↑n) else match ONote.split' a with | (a', m) => (ONote.oadd (e - 1) n a', m)

def ONote.split : ONote → ONote × ℕ

Calculate division and remainder of o mod ω. split o = (a, n) means o = a + n, where ω ∣ a.

Equations

• ONote.split ONote.zero = (0, 0)
• ONote.split (ONote.oadd e n a) = if e = 0 then (0, ↑n) else match ONote.split a with | (a', m) => (ONote.oadd e n a', m)

def ONote.scale (x : ONote) : ONote → ONote

scale x o is the ordinal notation for ω ^ x * o.

Equations

• ONote.scale x ONote.zero = 0
• ONote.scale x (ONote.oadd e n a) = ONote.oadd (x + e) n (ONote.scale x a)

def ONote.mulNat : ONote → ℕ → ONote

mulNat o n is the ordinal notation for o * n.

Equations

• ONote.mulNat x✝ x = match x✝, x with | ONote.zero, x => 0 | x, 0 => 0 | ONote.oadd e n a, Nat.succ m => ONote.oadd e (n * Nat.succPNat m) a

def ONote.opowAux (e : ONote) (a0 : ONote) (a : ONote) : ℕ → ℕ → ONote

Auxiliary definition to compute the ordinal notation for the ordinal exponentiation in opow

Equations

• ONote.opowAux e a0 a x 0 = 0
• ONote.opowAux e a0 a 0 (Nat.succ m) = ONote.oadd e (Nat.succPNat m) 0
• ONote.opowAux e a0 a (Nat.succ k) x = ONote.scale (e + ONote.mulNat a0 k) a + ONote.opowAux e a0 a k x

def ONote.opowAux2 (o₂ : ONote) (o₁ : ONote × ℕ) : ONote

Auxiliary definition to compute the ordinal notation for the ordinal exponentiation in opow

Equations

• One or more equations did not get rendered due to their size.

def ONote.opow (o₁ : ONote) (o₂ : ONote) : ONote

opow o₁ o₂ calculates the ordinal notation for the ordinal exponential o₁ ^ o₂.

Equations

• ONote.opow o₁ o₂ = ONote.opowAux2 o₂ (ONote.split o₁)

instance ONote.instPowONote : Pow ONote ONote

Equations

• ONote.instPowONote = { pow := ONote.opow }

theorem ONote.opow_def (o₁ : ONote) (o₂ : ONote) : o₁ ^ o₂ = ONote.opowAux2 o₂ (ONote.split o₁)

theorem ONote.split_eq_scale_split' {o : ONote} {o' : ONote} {m : ℕ} [ONote.NF o] : ONote.split' o = (o', m) → ONote.split o = (ONote.scale 1 o', m)

theorem ONote.nf_repr_split' {o : ONote} {o' : ONote} {m : ℕ} [ONote.NF o] : ONote.split' o = (o', m) → ONote.NF o' ∧ ONote.repr o = Ordinal.omega * ONote.repr o' + ↑m

theorem ONote.scale_eq_mul (x : ONote) [ONote.NF x] (o : ONote) [ONote.NF o] : ONote.scale x o = ONote.oadd x 1 0 * o

instance ONote.nf_scale (x : ONote) [ONote.NF x] (o : ONote) [ONote.NF o] : ONote.NF (ONote.scale x o)

Equations

• (_ : ONote.NF (ONote.scale x o)) = (_ : ONote.NF (ONote.scale x o))

@[simp]

theorem ONote.repr_scale (x : ONote) [ONote.NF x] (o : ONote) [ONote.NF o] : ONote.repr (ONote.scale x o) = Ordinal.omega ^ ONote.repr x * ONote.repr o

theorem ONote.nf_repr_split {o : ONote} {o' : ONote} {m : ℕ} [ONote.NF o] (h : ONote.split o = (o', m)) : ONote.NF o' ∧ ONote.repr o = ONote.repr o' + ↑m

theorem ONote.split_dvd {o : ONote} {o' : ONote} {m : ℕ} [ONote.NF o] (h : ONote.split o = (o', m)) : Ordinal.omega ∣ ONote.repr o'

theorem ONote.split_add_lt {o : ONote} {e : ONote} {n : ℕ+} {a : ONote} {m : ℕ} [ONote.NF o] (h : ONote.split o = (ONote.oadd e n a, m)) : ONote.repr a + ↑m < Ordinal.omega ^ ONote.repr e

@[simp]

theorem ONote.mulNat_eq_mul (n : ℕ) (o : ONote) : ONote.mulNat o n = o * ↑n

instance ONote.nf_mulNat (o : ONote) [ONote.NF o] (n : ℕ) : ONote.NF (ONote.mulNat o n)

Equations

• (_ : ONote.NF (ONote.mulNat o n)) = (_ : ONote.NF (ONote.mulNat o n))

instance ONote.nf_opowAux (e : ONote) (a0 : ONote) (a : ONote) [ONote.NF e] [ONote.NF a0] [ONote.NF a] (k : ℕ) (m : ℕ) : ONote.NF (ONote.opowAux e a0 a k m)

Equations

• (_ : ONote.NF (ONote.opowAux e a0 a k m)) = (_ : ONote.NF (ONote.opowAux e a0 a k m))

instance ONote.nf_opow (o₁ : ONote) (o₂ : ONote) [ONote.NF o₁] [ONote.NF o₂] : ONote.NF (o₁ ^ o₂)

Equations

• (_ : ONote.NF (o₁ ^ o₂)) = (_ : ONote.NF (o₁ ^ o₂))

theorem ONote.scale_opowAux (e : ONote) (a0 : ONote) (a : ONote) [ONote.NF e] [ONote.NF a0] [ONote.NF a] (k : ℕ) (m : ℕ) : ONote.repr (ONote.opowAux e a0 a k m) = Ordinal.omega ^ ONote.repr e * ONote.repr (ONote.opowAux 0 a0 a k m)

theorem ONote.repr_opow_aux₁ {e : ONote} {a : ONote} [Ne : ONote.NF e] [Na : ONote.NF a] {a' : Ordinal.{0}} (e0 : ONote.repr e ≠ 0) (h : a' < Ordinal.omega ^ ONote.repr e) (aa : ONote.repr a = a') (n : ℕ+) : (Ordinal.omega ^ ONote.repr e * ↑↑n + a') ^ Ordinal.omega = (Ordinal.omega ^ ONote.repr e) ^ Ordinal.omega

theorem ONote.repr_opow_aux₂ {a0 : ONote} {a' : ONote} [N0 : ONote.NF a0] [Na' : ONote.NF a'] (m : ℕ) (d : Ordinal.omega ∣ ONote.repr a') (e0 : ONote.repr a0 ≠ 0) (h : ONote.repr a' + ↑m < Ordinal.omega ^ ONote.repr a0) (n : ℕ+) (k : ℕ) : let R := ONote.repr (ONote.opowAux 0 a0 (ONote.oadd a0 n a' * ↑m) k m); (k ≠ 0 → R < (Ordinal.omega ^ ONote.repr a0) ^ Order.succ ↑k) ∧ (Ordinal.omega ^ ONote.repr a0) ^ ↑k * (Ordinal.omega ^ ONote.repr a0 * ↑↑n + ONote.repr a') + R = (Ordinal.omega ^ ONote.repr a0 * ↑↑n + ONote.repr a' + ↑m) ^ Order.succ ↑k

theorem ONote.repr_opow (o₁ : ONote) (o₂ : ONote) [ONote.NF o₁] [ONote.NF o₂] : ONote.repr (o₁ ^ o₂) = ONote.repr o₁ ^ ONote.repr o₂

def ONote.fundamentalSequence : ONote → Option ONote ⊕ (ℕ → ONote)

Given an ordinal, returns inl none for 0, inl (some a) for a+1, and inr f for a limit ordinal a, where f i is a sequence converging to a.

Equations

• One or more equations did not get rendered due to their size.
• ONote.fundamentalSequence ONote.zero = Sum.inl none

def ONote.FundamentalSequenceProp (o : ONote) : Option ONote ⊕ (ℕ → ONote) → Prop

The property satisfied by fundamentalSequence o:

• inl none means o = 0
• inl (some a) means o = succ a
• inr f means o is a limit ordinal and f is a strictly increasing sequence which converges to o

Equations

• One or more equations did not get rendered due to their size.

theorem ONote.fundamentalSequenceProp_inl_none (o : ONote) : ONote.FundamentalSequenceProp o (Sum.inl none) ↔ o = 0

theorem ONote.fundamentalSequenceProp_inl_some (o : ONote) (a : ONote) : ONote.FundamentalSequenceProp o (Sum.inl (some a)) ↔ ONote.repr o = Order.succ (ONote.repr a) ∧ (ONote.NF o → ONote.NF a)

theorem ONote.fundamentalSequenceProp_inr (o : ONote) (f : ℕ → ONote) : ONote.FundamentalSequenceProp o (Sum.inr f) ↔ Ordinal.IsLimit (ONote.repr o) ∧ (∀ (i : ℕ), f i < f (i + 1) ∧ f i < o ∧ (ONote.NF o → ONote.NF (f i))) ∧ ∀ a < ONote.repr o, ∃ (i : ℕ), a < ONote.repr (f i)

theorem ONote.fundamentalSequence_has_prop (o : ONote) : ONote.FundamentalSequenceProp o (ONote.fundamentalSequence o)

def ONote.fastGrowing : ONote → ℕ → ℕ

The fast growing hierarchy for ordinal notations < ε₀. This is a sequence of functions ℕ → ℕ indexed by ordinals, with the definition:

• f_0(n) = n + 1
• f_(α+1)(n) = f_α^[n](n)
• f_α(n) = f_(α[n])(n) where α is a limit ordinal and α[i] is the fundamental sequence converging to α

Equations

• One or more equations did not get rendered due to their size.

theorem ONote.fastGrowing_def {o : ONote} {x : Option ONote ⊕ (ℕ → ONote)} (e : ONote.fundamentalSequence o = x) : ONote.fastGrowing o = match (motive := (x : Option ONote ⊕ (ℕ → ONote)) → ONote.FundamentalSequenceProp o x → ℕ → ℕ) x, (_ : ONote.FundamentalSequenceProp o x) with | Sum.inl none, x => Nat.succ | Sum.inl (some a), x => fun (i : ℕ) => (ONote.fastGrowing a)^[i] i | Sum.inr f, x => fun (i : ℕ) => ONote.fastGrowing (f i) i

theorem ONote.fastGrowing_zero' (o : ONote) (h : ONote.fundamentalSequence o = Sum.inl none) : ONote.fastGrowing o = Nat.succ

theorem ONote.fastGrowing_succ (o : ONote) {a : ONote} (h : ONote.fundamentalSequence o = Sum.inl (some a)) : ONote.fastGrowing o = fun (i : ℕ) => (ONote.fastGrowing a)^[i] i

theorem ONote.fastGrowing_limit (o : ONote) {f : ℕ → ONote} (h : ONote.fundamentalSequence o = Sum.inr f) : ONote.fastGrowing o = fun (i : ℕ) => ONote.fastGrowing (f i) i

@[simp]

theorem ONote.fastGrowing_zero : ONote.fastGrowing 0 = Nat.succ

@[simp]

theorem ONote.fastGrowing_one : ONote.fastGrowing 1 = fun (n : ℕ) => 2 * n

@[simp]

theorem ONote.fastGrowing_two : ONote.fastGrowing 2 = fun (n : ℕ) => 2 ^ n * n

def ONote.fastGrowingε₀ (i : ℕ) : ℕ

We can extend the fast growing hierarchy one more step to ε₀ itself, using ω^(ω^...^ω^0) as the fundamental sequence converging to ε₀ (which is not an onote). Extending the fast growing hierarchy beyond this requires a definition of fundamental sequence for larger ordinals.

Equations

• ONote.fastGrowingε₀ i = ONote.fastGrowing ((fun (a : ONote) => ONote.oadd a 1 0)^[i] 0) i

theorem ONote.fastGrowingε₀_zero : ONote.fastGrowingε₀ 0 = 1

theorem ONote.fastGrowingε₀_one : ONote.fastGrowingε₀ 1 = 2

theorem ONote.fastGrowingε₀_two : ONote.fastGrowingε₀ 2 = 2048

def NONote : Type

The type of normal ordinal notations. (It would have been nicer to define this right in the inductive type, but NF o requires repr which requires ONote, so all these things would have to be defined at once, which messes up the VM representation.)

Equations

• NONote = { o : ONote // ONote.NF o }

instance instDecidableEqNONote : DecidableEq NONote

Equations

• instDecidableEqNONote = id inferInstance

instance NONote.NF (o : NONote) : ONote.NF ↑o

Equations

• (_ : ONote.NF ↑o) = (_ : ONote.NF ↑o)

def NONote.mk (o : ONote) [h : ONote.NF o] : NONote

Construct a NONote from an ordinal notation (and infer normality)

Equations

• NONote.mk o = { val := o, property := h }

noncomputable def NONote.repr (o : NONote) : Ordinal.{0}

The ordinal represented by an ordinal notation. (This function is noncomputable because ordinal arithmetic is noncomputable. In computational applications NONote can be used exclusively without reference to ordinal, but this function allows for correctness results to be stated.)

Equations

• NONote.repr o = ONote.repr ↑o

instance NONote.instToStringNONote : ToString NONote

Equations

• NONote.instToStringNONote = { toString := fun (x : NONote) => ONote.toString ↑x }

instance NONote.instReprNONote : Repr NONote

Equations

• NONote.instReprNONote = { reprPrec := fun (x : NONote) (prec : ℕ) => ONote.repr' prec ↑x }

instance NONote.instPreorderNONote : Preorder NONote

Equations

• NONote.instPreorderNONote = Preorder.mk NONote.instPreorderNONote.proof_1 NONote.instPreorderNONote.proof_2

instance NONote.instZeroNONote : Zero NONote

Equations

• NONote.instZeroNONote = { zero := { val := 0, property := ONote.NF.zero } }

instance NONote.instInhabitedNONote : Inhabited NONote

Equations

• NONote.instInhabitedNONote = { default := 0 }

theorem NONote.lt_wf : WellFounded fun (x x_1 : NONote) => x < x_1

instance NONote.instWellFoundedLTNONoteToLTInstPreorderNONote : WellFoundedLT NONote

Equations

• NONote.instWellFoundedLTNONoteToLTInstPreorderNONote = (_ : IsWellFounded NONote fun (x x_1 : NONote) => x < x_1)

instance NONote.instWellFoundedRelationNONote : WellFoundedRelation NONote

Equations

• NONote.instWellFoundedRelationNONote = { rel := fun (x x_1 : NONote) => x < x_1, wf := NONote.lt_wf }

def NONote.ofNat (n : ℕ) : NONote

Convert a natural number to an ordinal notation

Equations

• NONote.ofNat n = { val := ↑n, property := (_ : ONote.NF ↑n) }

def NONote.cmp (a : NONote) (b : NONote) : Ordering

Compare ordinal notations

Equations

• NONote.cmp a b = ONote.cmp ↑a ↑b

theorem NONote.cmp_compares (a : NONote) (b : NONote) : Ordering.Compares (NONote.cmp a b) a b

instance NONote.instLinearOrderNONote : LinearOrder NONote

Equations

• NONote.instLinearOrderNONote = linearOrderOfCompares NONote.cmp NONote.cmp_compares

instance NONote.instIsWellOrderNONoteLtToLTInstPreorderNONote : IsWellOrder NONote fun (x x_1 : NONote) => x < x_1

Equations

• NONote.instIsWellOrderNONoteLtToLTInstPreorderNONote = (_ : IsWellOrder NONote fun (x x_1 : NONote) => x < x_1)

def NONote.below (a : NONote) (b : NONote) : Prop

Asserts that repr a < ω ^ repr b. Used in NONote.recOn

Equations

• NONote.below a b = ONote.NFBelow (↑a) (NONote.repr b)

def NONote.oadd (e : NONote) (n : ℕ+) (a : NONote) (h : NONote.below a e) : NONote

The oadd pseudo-constructor for NONote

Equations

• NONote.oadd e n a h = { val := ONote.oadd (↑e) n ↑a, property := (_ : ONote.NF (ONote.oadd (↑e) n ↑a)) }

def NONote.recOn {C : NONote → Sort u_1} (o : NONote) (H0 : C 0) (H1 : (e : NONote) → (n : ℕ+) → (a : NONote) → (h : NONote.below a e) → C e → C a → C (NONote.oadd e n a h)) : C o

This is a recursor-like theorem for NONote suggesting an inductive definition, which can't actually be defined this way due to conflicting dependencies.

Equations

• One or more equations did not get rendered due to their size.

instance NONote.instAddNONote : Add NONote

Addition of ordinal notations

Equations

• NONote.instAddNONote = { add := fun (x y : NONote) => NONote.mk (↑x + ↑y) }

theorem NONote.repr_add (a : NONote) (b : NONote) : NONote.repr (a + b) = NONote.repr a + NONote.repr b

instance NONote.instSubNONote : Sub NONote

Subtraction of ordinal notations

Equations

• NONote.instSubNONote = { sub := fun (x y : NONote) => NONote.mk (↑x - ↑y) }

theorem NONote.repr_sub (a : NONote) (b : NONote) : NONote.repr (a - b) = NONote.repr a - NONote.repr b

instance NONote.instMulNONote : Mul NONote

Multiplication of ordinal notations

Equations

• NONote.instMulNONote = { mul := fun (x y : NONote) => NONote.mk (↑x * ↑y) }

theorem NONote.repr_mul (a : NONote) (b : NONote) : NONote.repr (a * b) = NONote.repr a * NONote.repr b

def NONote.opow (x : NONote) (y : NONote) : NONote

Exponentiation of ordinal notations

Equations

• NONote.opow x y = NONote.mk (↑x ^ ↑y)

theorem NONote.repr_opow (a : NONote) (b : NONote) : NONote.repr (NONote.opow a b) = NONote.repr a ^ NONote.repr b