Ordinal.CNF_sorted
theorem Ordinal.CNF_sorted :
∀ (b o : Ordinal.{u_1}), List.Sorted (fun x x_1 => x > x_1) (List.map Prod.fst (b.CNF o))
This theorem, `Ordinal.CNF_sorted`, states that for any two ordinals `b` and `o`, the list of first elements (or exponents) of the Cantor Normal Form (CNF) of `o` with base `b` are sorted in decreasing order. More explicitly, it means that every element in this list is strictly greater than the one that follows it. In other words, the exponents in the Cantor Normal Form of an ordinal, when the form has a specified base, form a decreasing sequence. The Cantor Normal Form is a unique representation of ordinals, and this property helps in its uniqueness and computation.
More concisely: For any ordinal `o` and base `b`, the exponents in the Cantor Normal Form of `o` with base `b` are strictly decreasing.
|
Ordinal.CNF_fst_le_log
theorem Ordinal.CNF_fst_le_log : ∀ {b o : Ordinal.{u}} {x : Ordinal.{u} × Ordinal.{u}}, x ∈ b.CNF o → x.1 ≤ b.log o
This theorem states that for any two ordinals `b` and `o` and any pair `x` of ordinals, if `x` is an element in the Cantor normal form representation of `o` with base `b` (denoted `b.CNF o`), then the first component of `x` (i.e., `x.1`) is less than or equal to the logarithm base `b` of `o` (denoted `b.log o`). In mathematical terms, this corresponds to saying that every exponent in the Cantor normal form of an ordinal is less than or equal to the logarithm of the ordinal with respect to the base of the Cantor normal form.
More concisely: For any ordinal `o` represented in Cantor normal form with base `b` as `b.CNF o = (x, y)`, the exponent `x` satisfies `x ≤ b.log o`.
|
Ordinal.CNF_foldr
theorem Ordinal.CNF_foldr : ∀ (b o : Ordinal.{u_1}), List.foldr (fun p r => b ^ p.1 * p.2 + r) 0 (b.CNF o) = o := by
sorry
This theorem, known as `Ordinal.CNF_foldr`, states that for any two ordinals `b` and `o` in a given Universe `u_1`, the evaluation of the Cantor Normal Form of `o` with respect to `b` gives back `o`. The Cantor Normal Form of `o` is evaluated using a right-associative fold operation, where each element of the Cantor Normal Form list (represented as a pair `p`) is processed by taking `b` to the power of the first element of `p`, multiplying it by the second element of `p`, and adding the result to the accumulated value `r`. This operation starts with an accumulated value of `0`.
More concisely: For any ordinal `o` and base `b` in a given universe, the right-associative fold operation of applying `b` raised to the first element and multiplying the result by the second element of each pair in the Cantor Normal Form of `o` equals `o`.
|
Ordinal.CNF_snd_lt
theorem Ordinal.CNF_snd_lt : ∀ {b o : Ordinal.{u}}, 1 < b → ∀ {x : Ordinal.{u} × Ordinal.{u}}, x ∈ b.CNF o → x.2 < b
This theorem, `Ordinal.CNF_snd_lt`, states that for any two ordinals `b` and `o`, where `b` is greater than 1, and for any pair of ordinals `x`, if `x` is an element of the Cantor normal form (CNF) of `o` with base `b`, then the second component of `x` is less than `b`. In other words, all coefficients in the Cantor normal form of an ordinal `o` with respect to a base `b` are strictly less than `b`.
More concisely: For any ordinal `o` and base `b` greater than 1, all coefficients in the Cantor normal form representation of `o` with respect to `b` are strictly less than `b`.
|
Ordinal.CNF_lt_snd
theorem Ordinal.CNF_lt_snd : ∀ {b o : Ordinal.{u}} {x : Ordinal.{u} × Ordinal.{u}}, x ∈ b.CNF o → 0 < x.2
This theorem states that every coefficient in a Cantor normal form is positive. In a more detailed description, for any two ordinals `b` and `o` and a pair of ordinals `x`, if `x` belongs to the Cantor normal form of `o` with base `b`, then the second element of `x` is greater than zero. This is a key property of Cantor normal forms, which are a specific representation of ordinal numbers.
More concisely: In the Cantor normal form representation of an ordinal number `o` with base `b`, every coefficient `x` has a positive second component.
|
Ordinal.CNF_fst_le
theorem Ordinal.CNF_fst_le : ∀ {b o : Ordinal.{u}} {x : Ordinal.{u} × Ordinal.{u}}, x ∈ b.CNF o → x.1 ≤ o
This theorem, named `Ordinal.CNF_fst_le`, states that for any pair of ordinals `b` and `o`, and any pair `x` of `Ordinal` type, if `x` is an element of the Cantor Normal Form (denoted as `CNF`) representation of `o` with base `b`, then the first component of `x` is less than or equal to `o`. The Cantor Normal Form is a unique representation of ordinals in terms of a base ordinal and exponents, and in this context, the theorem assures that no exponent in this representation can exceed the ordinal being represented.
More concisely: For any ordinal `o` represented in Cantor Normal Form with base `b` and any pair `x` in its representation, the first component of `x` is less than or equal to `o`.
|
Ordinal.CNF_zero
theorem Ordinal.CNF_zero : ∀ (b : Ordinal.{u_1}), b.CNF 0 = []
The theorem `Ordinal.CNF_zero` asserts that for all ordinals `b`, the Cantor Normal Form (CNF) of the ordinal `0` with respect to the base `b` is an empty list. In other words, when the ordinal that we are trying to express in Cantor Normal Form is `0`, regardless of what the base ordinal is, the CNF representation will always be an empty list.
More concisely: For all base ordinals `b`, the Cantor Normal Form of the ordinal `0` is the empty list.
|
Ordinal.CNF_ne_zero
theorem Ordinal.CNF_ne_zero :
∀ {b o : Ordinal.{u_1}}, o ≠ 0 → b.CNF o = (b.log o, o / b ^ b.log o) :: b.CNF (o % b ^ b.log o)
This theorem presents a recursive definition for the Cantor normal form of an ordinal `o` under the base `b`. When `o` is not zero, the Cantor normal form of `o` is a list starting with the pair `(Ordinal.log b o, o / b ^ Ordinal.log b o)`, followed by the Cantor normal form of the remainder when `o` is divided by `b` to the power of `Ordinal.log b o`. In other words, it breaks down `o` into a series of terms of the form 'base to the power of x, times y', and describes the Cantor normal form of `o` in terms of these terms. It's a way of representing the structure of the ordinal `o` in terms of the ordinal `b`.
More concisely: The Cantor normal form of a non-zero ordinal `o` under base `b` is a recursively defined list starting with `(log_b o, o % (b ^ log_b o))` and the Cantor normal form of `o % (b ^ log_b o)` under base `b`.
|