ONote.fastGrowing_def
theorem ONote.fastGrowing_def :
∀ {o : ONote} {x : Option ONote ⊕ (ℕ → ONote)} (e : o.fundamentalSequence = x),
o.fastGrowing =
match (motive := (x : Option ONote ⊕ (ℕ → ONote)) → o.FundamentalSequenceProp x → ℕ → ℕ) x, ⋯ with
| Sum.inl none, x => Nat.succ
| Sum.inl (some a), x => fun i => a.fastGrowing^[i] i
| Sum.inr f, x => fun i => (f i).fastGrowing i
This theorem, `ONote.fastGrowing_def`, describes the definition of the fast-growing hierarchy in ordinal notation. Given any ordinal notation `o` and a value `x`, which is either an optional ordinal notation or a function from natural numbers to ordinal notation, such that `x` equals the fundamental sequence of `o`, this theorem defines the fast-growing function on `o`. If `x` is `none`, the function is the successor function on natural numbers. If `x` is an ordinal notation `a`, the function is the iterated fast-growing function on `a`. If `x` is a function from natural numbers to ordinal notations, the function is a sequence of fast-growing functions indexed by natural numbers.
More concisely: The theorem `ONote.fastGrowing_def` defines the fast-growing function on an ordinal `o` as the successor function on natural numbers if `o` is undefined, the iterated fast-growing function on `o` if `o` is defined as an ordinal, or a sequence of fast-growing functions indexed by natural numbers if `o` is defined as a function from natural numbers to ordinal notations.
|
ONote.fastGrowing_succ
theorem ONote.fastGrowing_succ :
∀ (o : ONote) {a : ONote},
o.fundamentalSequence = Sum.inl (some a) → o.fastGrowing = fun i => a.fastGrowing^[i] i
This theorem, `ONote.fastGrowing_succ`, states that for any ordinal notation `o` and another ordinal notation `a`, if the fundamental sequence of `o` is the left sum of `some a`, then the fast-growing function of `o` is equivalent to the `i`-th iterate of the fast-growing function of `a` evaluated at `i`. Essentially, it relates the fast-growing function of an ordinal with the fast-growing functions of its fundamental sequences.
More concisely: For any ordinal notations `o` and `a`, if the fundamental sequence of `o` is the left sum of some `a`, then the fast-growing function of `o` is equivalent to the iterated fast-growing function of `a` evaluated at the index of the left sum.
|
ONote.NFBelow.repr_lt
theorem ONote.NFBelow.repr_lt : ∀ {o : ONote} {b : Ordinal.{0}}, o.NFBelow b → o.repr < Ordinal.omega ^ b
This theorem states that for any ordinal notation `o` and any ordinal `b` in the base universe, if the normal form of `o` is strictly below `b`, then the ordinal represented by `o` is strictly less than omega (the first infinite ordinal) raised to the power of `b`. In mathematical terms, if `o` is an ordinal notation and `b` is an ordinal such that the normal form of `o` is less than `b`, then the ordinal corresponding to `o` is less than ω^b, where ω is the ordinal corresponding to the set of natural numbers.
More concisely: For any ordinal notation `o` and ordinal `b`, if the normal form of `o` is strictly less than `b`, then the ordinal represented by `o` is strictly less than the ordinal ω^b.
|
ONote.NF.oadd
theorem ONote.NF.oadd : ∀ {e a : ONote}, e.NF → ∀ (n : ℕ+), a.NFBelow e.repr → (e.oadd n a).NF
This theorem states that for any ordinal numbers 'e' and 'a', if 'e' is normal form (ONote.NF e) and 'n' is a positive natural number such that 'a' is below 'e' in the fast-growing hierarchy (ONote.NFBelow a (ONote.repr e)), then the ordinal notation 'oadd e n a' is also in normal form (ONote.NF (ONote.oadd e n a)).
In other words, it asserts that if an ordinal 'e' is in normal form, and 'a' is below 'e' in the fast-growing hierarchy, then the ordinal formed by the ordinal addition operation with 'e', 'n', and 'a' is also in normal form.
More concisely: If an ordinal 'e' is in normal form and 'a' is below 'e' in the fast-growing hierarchy, then the ordinal obtained by adding 'n' to 'e' (where 'n' is a positive natural number) is also in normal form.
|
ONote.cmp_compares
theorem ONote.cmp_compares : ∀ (a b : ONote) [inst : a.NF] [inst : b.NF], (a.cmp b).Compares a b
The theorem `ONote.cmp_compares` states that for any two ordinal notes `a` and `b`, where both `a` and `b` are in "normal form" (this is denoted by `[inst : ONote.NF a] [inst : ONote.NF b]` - it's a kind of precondition), the `Ordering.Compares` function with the comparison of `a` and `b` as the first argument, and `a` and `b` as the second and third arguments, holds true. In other words, this theorem guarantees that the comparison function `ONote.cmp` on ordinal notes in normal form aligns with the standard ordering comparison between `a` and `b`.
More concisely: For any ordinal notes `a` and `b` in normal form, `Ordering.compares a b <-> ONote.cmp a b` holds true.
|
ONote.omega_le_oadd
theorem ONote.omega_le_oadd : ∀ (e : ONote) (n : ℕ+) (a : ONote), Ordinal.omega ^ e.repr ≤ (e.oadd n a).repr
The theorem `ONote.omega_le_oadd` states that for any ordinal number `e`, a natural number `n` greater than zero, and another ordinal number `a`, the ordinal ω (omega), raised to the ordinal denoted by `e`, is less than or equal to the ordinal denoted by the ONote that adds `e`, `n`, and `a`. In other words, ω^e ≤ the ordinal represented by oadd(e, n, a). Here, ω represents the first infinite ordinal, defined as the order type of natural numbers. ONote is a structure used to denote ordinals in Lean 4, and ONote.repr returns the ordinal denoted by a given ONote.
More concisely: For any ordinal numbers `e`, `n` > 0, and `a`, the ordinal ω^e is less than or equal to the ordinal represented by ONote.oadd(e, n, a).
|
ONote.lt_def
theorem ONote.lt_def : ∀ {x y : ONote}, x < y ↔ x.repr < y.repr
The theorem `ONote.lt_def` states that for any two ordinal notations `x` and `y`, `x` is less than `y` if and only if the ordinal represented by `x` is less than the ordinal represented by `y`. Here, `ONote.repr` is a function that takes an ordinal notation and returns the corresponding ordinal. The comparison between `x` and `y` is made in terms of the mathematical concept of ordinal numbers, which generalize the concept of natural numbers to include notions of "infinity" and their arithmetic.
More concisely: For any ordinal notations x and y, x < y if and only if ONote.repr x < ONote.repr y.
|
ONote.NF.snd'
theorem ONote.NF.snd' : ∀ {e : ONote} {n : ℕ+} {a : ONote}, (e.oadd n a).NF → a.NFBelow e.repr
The theorem `ONote.NF.snd'` states that for any ordinal notation `e`, positive natural number `n`, and ordinal notation `a`, if the ordinal notation constructed from `e`, `n`, and `a` (in the form `ONote.oadd e n a`) is in normal form (`ONote.NF`), then the ordinal notation `a` is below the ordinal representation of `e` (`ONote.repr e`) in terms of normal form (`ONote.NFBelow`). Here, "normal form" indicates a specific format for expressing ordinal notations, and "below" means that `a` is less than or equal to `e` in the ordering defined by this normal form.
More concisely: For any ordinal notations `e`, `n`, and `a` in normal form, if `ONote.oadd e n a` is equal to `ONote.NF (ONote.oadd e n a)`, then `a` is below `e` in the normal form ordering.
|
ONote.fundamentalSequence_has_prop
theorem ONote.fundamentalSequence_has_prop : ∀ (o : ONote), o.FundamentalSequenceProp o.fundamentalSequence
This theorem, named `ONote.fundamentalSequence_has_prop`, states that for any ordinal notation `o`, the fundamental sequence of `o` satisfies the fundamental sequence property of `o`. In other words, for every ordinal notation, the fundamental sequence associated with it fulfills the property that the `ONote` class defines as fundamental.
More concisely: For every ordinal notation `o`, the fundamental sequence of `o` is a sequence that satisfies the fundamental sequence property defined by the `ONote` class.
|
ONote.NF.below_of_lt
theorem ONote.NF.below_of_lt :
∀ {e : ONote} {n : ℕ+} {a : ONote} {b : Ordinal.{0}}, e.repr < b → (e.oadd n a).NF → (e.oadd n a).NFBelow b := by
sorry
The theorem `ONote.NF.below_of_lt` expresses that for any ordinal numbers `e` and `a`, any positive natural number `n`, and any ordinal `b` in Type 0, if the ordinal represented by `e` is less than `b`, and the ordinal `ONote.oadd e n a` is in Normal Form (meaning that it is in Cantor Normal Form which is a specific representation of ordinals), then `ONote.oadd e n a` is strictly below `b` in the ordinal hierarchy. In other words, the ordinal composed of `e`, `n`, and `a` is less than `b` when `e` is less than `b` and the ordinal composed of `e`, `n`, and `a` adheres to the properties of the Normal Form.
More concisely: If `e` is less than `b` and `ONote.NF.is_normal (ONote.oadd e n a)` holds, then `ONote.oadd e n a` is strictly below `b` in the ordinal hierarchy.
|