The ray of a front

Given a front F on M and a node [a] of its tree (i.e. a is the least element of some element of F), the ray F after a (terminology from the author's EMS survey Towards better: A motivated introduction to better-quasi-orders) is the front obtained by stripping the leading a from the elements of F that start with a. It is a front on M after a, the infinite set {n ∈ M : n > a}, itself represented enumeration-first as the subsequence M ∘ (· + j) where j is the least index at which M passes a.

("Ray" is not to be confused with the derivative, the tree-to-tree leaf-removal operation whose iteration computes the rank.)

Main definitions

• rayEnum M a : the enumeration M ∘ (· + afterShift M a) of {n ∈ M : n > a} (front- independent).
• Front.ray F a : the ray {t | a :: t ∈ F}.

Main results

• Front.ray_isFront : the ray F after a is a front on M after a.
• Front.IsFront.singleton_mem_tree : in a nontrivial front ([] ∉ F) every n ∈ M heads an element, i.e. [n] ∈ tree F.
• Front.IsFront.ray_isFront_mem : for a nontrivial front and n ∈ M, F after n is a front on M after n.

Nontriviality

The trivial front is {[]} (rank 0). For a front, [] ∉ F, F ≠ {[]}, ⋃ F = M, and "[n] ∈ tree F for every n ∈ M" are all equivalent; [] ∉ F is the canonical working flag (see IsFront.nil_not_mem_iff).

Enumeration operations

afterShift and rayEnum operate on a strictly monotone enumeration M : ℕ → ℕ; they do not depend on any front, so they live outside the Front namespace.

noncomputable def afterShift (M : ℕ → ℕ) (a : ℕ) : ℕ

The least index at which M passes a.

Equations

• afterShift M a = sInf {j : ℕ | a < M j}

noncomputable def rayEnum (M : ℕ → ℕ) (a : ℕ) : ℕ → ℕ

M after a: the increasing enumeration of {n ∈ M : n > a}, as the subsequence M ∘ (· + afterShift M a). A StrictMono-to-StrictMono operation on enumerations.

Equations

• rayEnum M a i = M (i + afterShift M a)

theorem afterShift_spec {M : ℕ → ℕ} (hM : StrictMono M) (a : ℕ) : a < M (afterShift M a)

theorem lt_of_lt_afterShift {M : ℕ → ℕ} {a k : ℕ} (hk : k < afterShift M a) : M k ≤ a

theorem rayEnum_strictMono {M : ℕ → ℕ} (hM : StrictMono M) (a : ℕ) : StrictMono (rayEnum M a)

theorem rayEnum_gt {M : ℕ → ℕ} (hM : StrictMono M) (a i : ℕ) : a < rayEnum M a i

theorem rayEnum_mem_range {M : ℕ → ℕ} (a i : ℕ) : rayEnum M a i ∈ Set.range M

theorem mem_range_rayEnum_iff {M : ℕ → ℕ} (hM : StrictMono M) (a n : ℕ) : n ∈ Set.range (rayEnum M a) ↔ n ∈ Set.range M ∧ a < n

def Front.ray (F : Set (List ℕ)) (a : ℕ) : Set (List ℕ)

F after a (the ray of F at a): strip the leading a from the elements of F that start with a.

Equations

• Front.ray F a = {t : List ℕ | a :: t ∈ F}

theorem Front.exists_frontElem_isInit {M : ℕ → ℕ} {F : Set (List ℕ)} (hF : IsFront F M) {N : ℕ → ℕ} (hN : StrictMono N) (hsub : Set.range N ⊆ Set.range M) : ∃ u ∈ F, IsInit u N

Density transported: any strictly monotone subsequence of M has an initial segment in F.

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

theorem Front.IsFront.nil_not_mem_iff {M : ℕ → ℕ} {F : Set (List ℕ)} (hF : IsFront F M) : [] ∉ F ↔ F ≠ {[]}

A front is nontrivial ([] ∉ F) iff it is not the trivial front {[]}.

theorem Front.IsFront.singleton_mem_tree {M : ℕ → ℕ} {F : Set (List ℕ)} (hF : IsFront F M) (h0 : [] ∉ F) {n : ℕ} (hn : n ∈ Set.range M) : [n] ∈ tree F

In a nontrivial front, every element of M heads some element of F. For [] ∉ F and n ∈ M, the singleton [n] is a node of the tree of F.

theorem Front.exists_cons_mem {M : ℕ → ℕ} {F : Set (List ℕ)} (hF : IsFront F M) {a : ℕ} (ha : [a] ∈ tree F) {Q : ℕ → ℕ} (hQ : StrictMono Q) (haQ : a < Q 0) (hQM : ∀ (i : ℕ), Q i ∈ Set.range M) : ∃ (t : List ℕ), a :: t ∈ F ∧ IsInit t Q

The head-stripping construction: if [a] is in the tree and Q is a strictly monotone subsequence of M with a < Q 0, then some a :: t ∈ F with t an initial segment of Q.

theorem Front.ray_isFront {M : ℕ → ℕ} {F : Set (List ℕ)} (hF : IsFront F M) {a : ℕ} (ha : [a] ∈ tree F) : IsFront (ray F a) (rayEnum M a)

F after a is a front on M after a, whenever [a] is a node of the tree of F (i.e. a is the least element of some element of F).

theorem Front.IsFront.ray_isFront_mem {M : ℕ → ℕ} {F : Set (List ℕ)} (hF : IsFront F M) (h0 : [] ∉ F) {n : ℕ} (hn : n ∈ Set.range M) : IsFront (ray F n) (rayEnum M n)

For a nontrivial front and n ∈ M, F after n is a front on M after n.

Rank of the ray

The ray strictly lowers the rank. This is what makes the Nash-Williams recursion well-founded.

The tree of ray F a is the subtree of tree F sitting above the node [a], transported by t ↦ a :: t; mem_tree_ray is the membership bridge (the single point of contact with the concrete tree representation — a later switch to Descriptive.Tree.subAt would rewrite only this lemma).

theorem Front.mem_tree_ray {F : Set (List ℕ)} {a : ℕ} {t : List ℕ} : t ∈ tree (ray F a) ↔ a :: t ∈ tree F

The tree of the ray at a is tree F above [a], stripped of the leading a.

theorem Front.IsFront.ray_rank_lt {M : ℕ → ℕ} {F : Set (List ℕ)} (hF : IsFront F M) (h0 : [] ∉ F) {n : ℕ} (hn : n ∈ Set.range M) : ⋯.rank < hF.rank

The ray strictly lowers the rank. For a nontrivial front and n ∈ M, the front F after n has rank strictly below that of F.