The Kleene–Brouwer order on a tree

Pure combinatorics on Descriptive.tree ℕ (prefix-closed sets of List ℕ), no codes: the raw mathematics behind analytic boundedness for well-founded trees (issue #73).

• HasInfiniteBranch T is a descending chain in strict extension — a sequence of nodes each properly extending the previous — so "no infinite branch" is well-foundedness of extBelow T on the nose (wellFounded_extBelow_iff_not_hasInfiniteBranch), with no appeal to König.
• The Kleene–Brouwer order is the lexicographic order on List ℕ∞ pulled back along kbEncode x = x.map (↑) ++ [⊤]: appending ⊤ makes every proper extension of a node smaller than the node, and among incomparable nodes the leftmost first difference decides. Linearity is inherited (kbLinearOrder); kbLT_of_extBelow records that strict extension is a subrelation.
• wellFounded_kbLT: KB is well-founded on a well-founded tree. Along a strictly KB-descending sequence every k-prefix stabilizes (exists_stable_prefix): once the k-prefix is fixed, the k-th KB head is antitone in ℕ∞ and hence eventually constant, and it cannot stabilize at ⊤, since the sequence would then repeat a list. The stabilized prefixes form an infinite branch.
• treeHeight T is the strict supremum of the ranks of the nodes under strict extension, and treeHeight_le_type bounds it by the KB order type, through the monotonicity of IsWellFounded.rank in the relation (InfinitaryLogic.rank_le_rank_of_imp).

The encoding lands in ℕ∞, which is defined as WithTop ℕ; the named type is what carries the derived WellFoundedLT instance the chain condition uses.

Strict extension and branches

def KleeneBrouwer.ProperPrefix (x y : List ℕ) : Prop

x is a proper prefix of y.

Equations

• KleeneBrouwer.ProperPrefix x y = (x <+: y ∧ x ≠ y)

def KleeneBrouwer.ExtBelow (y x : List ℕ) : Prop

The "descending" direction for well-foundedness: y sits below x when it properly extends x.

Equations

• KleeneBrouwer.ExtBelow y x = KleeneBrouwer.ProperPrefix x y

def KleeneBrouwer.HasInfiniteBranch (T : ↥(Descriptive.tree ℕ)) : Prop

An infinite branch, as a descending chain in strict extension: a sequence of nodes of T each properly extending the previous one.

Equations

• KleeneBrouwer.HasInfiniteBranch T = ∃ (f : ℕ → List ℕ), (∀ (n : ℕ), f n ∈ T) ∧ ∀ (n : ℕ), KleeneBrouwer.ProperPrefix (f n) (f (n + 1))

def KleeneBrouwer.extBelow (T : ↥(Descriptive.tree ℕ)) (y x : ↥T) : Prop

The strict-extension relation restricted to the nodes of T.

Equations

• KleeneBrouwer.extBelow T y x = KleeneBrouwer.ExtBelow ↑y ↑x

theorem KleeneBrouwer.ProperPrefix.trans {x y z : List ℕ} (h₁ : ProperPrefix x y) (h₂ : ProperPrefix y z) : ProperPrefix x z

instance KleeneBrouwer.instIsStrictOrderSubtypeListNatMemSetCompleteSublatticeTreeExtBelow (T : ↥(Descriptive.tree ℕ)) : IsStrictOrder (↥T) (extBelow T)

theorem KleeneBrouwer.wellFounded_extBelow_iff_not_hasInfiniteBranch (T : ↥(Descriptive.tree ℕ)) : WellFounded (extBelow T) ↔ ¬HasInfiniteBranch T

The Kleene–Brouwer order, via lexicographic order on WithTop ℕ

def KleeneBrouwer.kbEncode (x : List ℕ) : List ℕ∞

Encode a node so that a proper prefix becomes larger than its extensions: append ⊤.

Equations

• KleeneBrouwer.kbEncode x = List.map (fun (a : ℕ) => ↑a) x ++ [⊤]

theorem KleeneBrouwer.kbEncode_injective : Function.Injective kbEncode

def KleeneBrouwer.KBLT (x y : List ℕ) : Prop

The Kleene–Brouwer order: proper extensions come first, then leftmost-first differences.

Equations

• KleeneBrouwer.KBLT x y = (KleeneBrouwer.kbEncode x < KleeneBrouwer.kbEncode y)

@[instance_reducible]

instance KleeneBrouwer.instDecidableRelListNatKBLT : DecidableRel KBLT

Equations

• KleeneBrouwer.instDecidableRelListNatKBLT x y = KleeneBrouwer.instDecidableRelListNatKBLT._aux_1 x y

@[instance_reducible]

instance KleeneBrouwer.instDecidableRelListNatKBLT_1 : DecidableRel KBLT

Equations

• KleeneBrouwer.instDecidableRelListNatKBLT_1 x y = KleeneBrouwer.instDecidableRelListNatKBLT_1._aux_1 x y

@[instance_reducible]

instance KleeneBrouwer.instDecidableRelListNatKBLT_2 : DecidableRel KBLT

Equations

• KleeneBrouwer.instDecidableRelListNatKBLT_2 x y = KleeneBrouwer.instDecidableRelListNatKBLT_2._aux_1 x y

def KleeneBrouwer.kbLT (T : ↥(Descriptive.tree ℕ)) (x y : ↥T) : Prop

The KB order on the nodes of T.

Equations

• KleeneBrouwer.kbLT T x y = KleeneBrouwer.KBLT ↑x ↑y

@[instance_reducible]

noncomputable def KleeneBrouwer.kbLinearOrder (T : ↥(Descriptive.tree ℕ)) : LinearOrder ↥T

The nodes of T, linearly ordered by KB (pulled back from List ℕ∞).

Equations

• KleeneBrouwer.kbLinearOrder T = LinearOrder.lift' (fun (x : ↥T) => KleeneBrouwer.kbEncode ↑x) ⋯

theorem KleeneBrouwer.kbLT_iff (T : ↥(Descriptive.tree ℕ)) (x y : ↥T) : kbLT T x y ↔ x < y

Proper extensions are KB-below

theorem KleeneBrouwer.kbEncode_lt_of_properPrefix {x y : List ℕ} (h : ProperPrefix x y) : kbEncode y < kbEncode x

theorem KleeneBrouwer.kbLT_of_extBelow (T : ↥(Descriptive.tree ℕ)) {y x : ↥T} (h : extBelow T y x) : kbLT T y x

KB is well-founded on a well-founded tree

theorem KleeneBrouwer.exists_stable_prefix {f : ℕ → List ℕ} (hf : ∀ (n : ℕ), KBLT (f (n + 1)) (f n)) (k : ℕ) : ∃ (p : List ℕ) (N : ℕ), p.length = k ∧ ∀ (n : ℕ), N ≤ n → List.take k (f n) = p

Prefix stabilization: along a strictly KB-descending sequence in a tree, every k-prefix is eventually constant, with full length k.

instance KleeneBrouwer.instIsStrictOrderSubtypeListNatMemSetCompleteSublatticeTreeKbLT (T : ↥(Descriptive.tree ℕ)) : IsStrictOrder (↥T) (kbLT T)

theorem KleeneBrouwer.wellFounded_kbLT (T : ↥(Descriptive.tree ℕ)) (hT : WellFounded (extBelow T)) : WellFounded (kbLT T)

Kleene–Brouwer is well-founded on a well-founded tree.

theorem KleeneBrouwer.isWellOrder_kbLT (T : ↥(Descriptive.tree ℕ)) (hT : WellFounded (extBelow T)) : IsWellOrder (↥T) (kbLT T)

KB is a well-order on a well-founded tree: the linear order from the encoding plus well-foundedness.

noncomputable def KleeneBrouwer.treeHeight (T : ↥(Descriptive.tree ℕ)) [IsWellFounded (↥T) (extBelow T)] : Ordinal.{0}

The height of the tree: the strict supremum of the ranks of its nodes under strict extension.

Equations

• KleeneBrouwer.treeHeight T = ⨆ (x : ↥T), Order.succ (IsWellFounded.rank (KleeneBrouwer.extBelow T) x)

theorem KleeneBrouwer.treeHeight_le_type (T : ↥(Descriptive.tree ℕ)) [IsWellFounded (↥T) (extBelow T)] [IsWellOrder (↥T) (kbLT T)] : treeHeight T ≤ Ordinal.type (kbLT T)

Given that KB is a well-order on T, the height is at most its order type.