The tree of a front is well-founded

The tree of a front F is the set of all prefixes (initial segments) of elements of F, ordered by proper end-extension (treeExt F a b : a properly extends b). This file proves that this relation is well-founded, so a front has an ordinal rank.

Well-foundedness is proved directly, by showing there is no infinite descending chain. A descending chain is an ascending tower f 0 ⊏ f 1 ⊏ ⋯ of proper extensions inside the tree. Its lengths grow without bound, so the tower has a limit b : ℕ → ℕ, a strictly increasing subsequence of M. By Density some t ∈ F is an initial segment of b; extending it by one more entry of b lands inside some u ∈ F with t <+: u, so Incomparability forces t = u — impossible, as u is strictly longer.

Main results

• Front.exists_strictMono_comp: a strictly monotone b with range b ⊆ range M is a subsequence M ∘ g of M (the enumeration bridge).
• Front.IsFront.wellFounded_treeExt: proper end-extension is well-founded on the tree of a front.
• Front.IsFront.rank: the ordinal rank of a front.
• Front.powK_rank: the uniform front [M]^k has rank k.
• Front.schreier_rank: the Schreier front has rank ω.

theorem RelHom.rank_le {α β : Type u} {r : α → α → Prop} {s : β → β → Prop} [IsWellFounded α r] [IsWellFounded β s] (f : r →r s) (a : α) : IsWellFounded.rank r a ≤ IsWellFounded.rank s (f a)

A relation homomorphism does not increase rank. If f : r →r s maps r into a well-founded relation s, then the r-rank of a is at most the s-rank of f a. This is the cross-relation companion to IsWellFounded.rank_lt_of_rel (which only compares ranks within a single relation), and the tool underlying the rank comparisons for the ray and the restriction of a front. General; Mathlib-bound (belongs next to IsWellFounded.rank_lt_of_rel).

def Front.tree (F : Set (List ℕ)) : Set (List ℕ)

The tree of a front F: all prefixes (initial segments) of elements of F.

Equations

• Front.tree F = {s : List ℕ | ∃ t ∈ F, s <+: t}

def Front.treeExt (F : Set (List ℕ)) (a b : List ℕ) : Prop

Proper end-extension inside the tree of F: treeExt F a b holds when a properly extends b and both lie in the tree. Its well-foundedness is what allows ranking a front. Note the recursion direction: IsWellFounded.rank (treeExt F) s is the supremum of succ (rank s') over the proper extensions s' of s, matching the usual rank of a front.

Equations

• Front.treeExt F a b = (a ∈ Front.tree F ∧ b ∈ Front.tree F ∧ b <+: a ∧ b ≠ a)

theorem Front.strictMono_of_pairwise_map {b : ℕ → ℕ} (h : ∀ (n : ℕ), List.Pairwise (fun (x1 x2 : ℕ) => x1 < x2) (List.map b (List.range n))) : StrictMono b

If every finite initial segment of b is strictly increasing, then b is strictly monotone.

theorem Front.exists_strictMono_comp {M b : ℕ → ℕ} (hM : StrictMono M) (hb : StrictMono b) (hsub : ∀ (i : ℕ), b i ∈ Set.range M) : ∃ (g : ℕ → ℕ), StrictMono g ∧ M ∘ g = b

Enumeration bridge. A strictly monotone b whose range is contained in that of a strictly monotone M is a subsequence M ∘ g of M, for a unique strictly monotone g.

theorem Front.IsFront.wellFounded_treeExt {F : Set (List ℕ)} {M : ℕ → ℕ} (hF : IsFront F M) : WellFounded (treeExt F)

Proper end-extension is well-founded on the tree of a front. Proved directly: there is no infinite descending chain.

noncomputable def Front.IsFront.rank {F : Set (List ℕ)} {M : ℕ → ℕ} (hF : IsFront F M) : Ordinal.{0}

The ordinal rank of a front: the rank of the root [] in the well-founded tree of proper end-extensions.

Equations

• hF.rank = IsWellFounded.rank (Front.treeExt F) []

theorem Front.IsFront.nil_mem_tree {F : Set (List ℕ)} {M : ℕ → ℕ} (hF : IsFront F M) : [] ∈ tree F

The root [] is in the tree of any front (fronts are nonempty by Density).

theorem Front.exists_gt_range {M : ℕ → ℕ} (hM : StrictMono M) (n : ℕ) : ∃ x ∈ Set.range M, n < x

M being a strictly monotone enumeration, there is an element of M above any bound.

theorem Front.exists_extend_gt {M : ℕ → ℕ} (hM : StrictMono M) (s : List ℕ) : ∃ x ∈ Set.range M, ∀ y ∈ s, y < x

An increasing list contained in M can be extended by one further element of M.

theorem Front.exists_extend_len {M : ℕ → ℕ} (hM : StrictMono M) (L : ℕ) (s : List ℕ) : List.Pairwise (fun (x1 x2 : ℕ) => x1 < x2) s → (∀ x ∈ s, x ∈ Set.range M) → s.length ≤ L → ∃ (t : List ℕ), s <+: t ∧ List.Pairwise (fun (x1 x2 : ℕ) => x1 < x2) t ∧ (∀ x ∈ t, x ∈ Set.range M) ∧ t.length = L

Any increasing list in M extends to an increasing list in M of any prescribed length.

theorem Front.rank_eq_sub {F : Set (List ℕ)} {M : ℕ → ℕ} (hF : IsFront F M) {s0 : List ℕ} (L : ℕ) (hbound : ∀ (s : List ℕ), s0 <+: s → s ∈ tree F → s.length ≤ L) (hext : ∀ (s : List ℕ), s0 <+: s → s ∈ tree F → s.length < L → ∃ (x : ℕ), treeExt F (s ++ [x]) s) (s : List ℕ) (hs0 : s0 <+: s) (hs : s ∈ tree F) : IsWellFounded.rank (treeExt F) s = ↑(L - s.length)

General rank formula. If, above a fixed node s0, every tree node has length ≤ L and every tree node of length < L has a one-step extension in the tree, then the rank of a node s above s0 is L - s.length.

theorem Front.mem_tree_powK {M : ℕ → ℕ} (hM : StrictMono M) {k : ℕ} {s : List ℕ} : s ∈ tree (powK M k) ↔ List.Pairwise (fun (x1 x2 : ℕ) => x1 < x2) s ∧ (∀ x ∈ s, x ∈ Set.range M) ∧ s.length ≤ k

Membership in the tree of [M]^k: increasing lists in M of length at most k.

theorem Front.powK_rank {M : ℕ → ℕ} (hM : StrictMono M) (k : ℕ) : ⋯.rank = ↑k

The uniform front [M]^k has rank k.

theorem Front.mem_tree_schreier {M : ℕ → ℕ} (hM : StrictMono M) {s : List ℕ} : s ∈ tree (schreier M) ↔ List.Pairwise (fun (x1 x2 : ℕ) => x1 < x2) s ∧ (∀ x ∈ s, x ∈ Set.range M) ∧ ∀ (a : ℕ), s.head? = some a → s.length ≤ a + 1

Membership in the tree of the Schreier front.

theorem Front.schreier_rank_node {M : ℕ → ℕ} (hM : StrictMono M) {s : List ℕ} {a : ℕ} (hsmem : s ∈ tree (schreier M)) (hhead : s.head? = some a) : IsWellFounded.rank (treeExt (schreier M)) s = ↑(a + 1 - s.length)

Interior of the Schreier front. A node s in the tree with first element a has rank a + 1 - s.length.

theorem Front.schreier_rank {M : ℕ → ℕ} (hM : StrictMono M) : ⋯.rank = Ordinal.omega0

The Schreier front has rank ω.