Positions of a Tree: the Inherited Order Stack

Branching.Positions t — the valid positions of a concrete tree, as a subtype of TreePath. Because validPaths is prefix-closed (validPaths_prefix_closed), the subtype inherits the full rooted-tree order stack from TreePath:

instance	reading
OrderBot	the root position
PredOrder	parent (mother-of) stays inside the tree
SemilatticeInf	least common ancestor stays inside the tree
IsPredArchimedean	finite ancestor chains

This makes the per-tree position type a rooted tree in mathlib's order-theoretic sense (Mathlib.Order.SuccPred.Tree), with parent, LCA, and the lattice lemma library available on any Branching carrier's positions.

The B&P bridge

TreeOrder.ofPredArchimedean connects the mathlib stack to [BP90]'s TreeOrder: any bottomed pred-archimedean partial order satisfies the Connected Ancestor Condition, because two ancestors of one node are both pred-iterates of it and hence comparable. B&P's structure is the strictly more general one (it admits dense dominance orders with no parent function); this is the general-structure-plus-specialization pattern, connected by construction rather than stipulation.

@[reducible, inline]

abbrev Core.Order.Branching.Positions {T : Type u_1} [Branching T] (t : T) : Type

The valid positions of t, as a subtype of TreePath. Inherits the rooted-tree order stack (root, parent, LCA, finite depth) from TreePath via prefix-closure.

Equations

• Core.Order.Branching.Positions t = { p : Core.Order.TreePath // p ∈ Core.Order.Branching.validPaths t }

@[implicit_reducible]

instance Core.Order.Branching.Positions.instPartialOrder {T : Type u_1} [Branching T] {t : T} : PartialOrder (Positions t)

Equations

• Core.Order.Branching.Positions.instPartialOrder = Subtype.partialOrder fun (p : Core.Order.TreePath) => p ∈ Core.Order.Branching.validPaths t

@[simp]

theorem Core.Order.Branching.Positions.mk_le_mk {T : Type u_1} [Branching T] {t : T} {p q : TreePath} {hp : p ∈ validPaths t} {hq : q ∈ validPaths t} : ⟨p, hp⟩ ≤ ⟨q, hq⟩ ↔ p ≤ q

@[simp]

theorem Core.Order.Branching.Positions.mk_lt_mk {T : Type u_1} [Branching T] {t : T} {p q : TreePath} {hp : p ∈ validPaths t} {hq : q ∈ validPaths t} : ⟨p, hp⟩ < ⟨q, hq⟩ ↔ p < q

@[implicit_reducible]

instance Core.Order.Branching.Positions.instOrderBot {T : Type u_1} [Branching T] {t : T} : OrderBot (Positions t)

The root position.

Equations

• Core.Order.Branching.Positions.instOrderBot = { bot := ⟨⊥, ⋯⟩, bot_le := ⋯ }

@[simp]

theorem Core.Order.Branching.Positions.bot_val {T : Type u_1} [Branching T] {t : T} : ↑⊥ = ⊥

@[implicit_reducible]

instance Core.Order.Branching.Positions.instSemilatticeInf {T : Type u_1} [Branching T] {t : T} : SemilatticeInf (Positions t)

Least common ancestor: the LCA of two valid positions is valid (it is an ancestor of either).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Core.Order.Branching.Positions.inf_val {T : Type u_1} [Branching T] {t : T} (p q : Positions t) : ↑(p ⊓ q) = ↑p ⊓ ↑q

@[implicit_reducible]

instance Core.Order.Branching.Positions.instPredOrder {T : Type u_1} [Branching T] {t : T} : PredOrder (Positions t)

Parent: the parent of a valid position is valid.

Equations

• Core.Order.Branching.Positions.instPredOrder = { pred := fun (p : Core.Order.Branching.Positions t) => ⟨(↑p).parent, ⋯⟩, pred_le := ⋯, min_of_le_pred := ⋯, le_pred_of_lt := ⋯ }

@[simp]

theorem Core.Order.Branching.Positions.pred_val {T : Type u_1} [Branching T] {t : T} (p : Positions t) : ↑(Order.pred p) = (↑p).parent

instance Core.Order.Branching.Positions.instIsPredArchimedean {T : Type u_1} [Branching T] {t : T} : IsPredArchimedean (Positions t)

Finite ancestor chains, inherited from TreePath.

def Core.Order.Branching.Positions.Positions.rootedTree {T : Type u_1} [Branching T] (t : T) : RootedTree

The positions of t as a mathlib RootedTree (Mathlib.Order.SuccPred.Tree): the inherited stack, bundled.

Equations

• One or more equations did not get rendered due to their size.

The B&P bridge

def Core.Order.TreeOrder.ofPredArchimedean (α : Type u_1) [PartialOrder α] [PredOrder α] [IsPredArchimedean α] [OrderBot α] : TreeOrder α

The mathlib-stack ⟹ B&P bridge: any bottomed pred-archimedean partial order is a [BP90] TreeOrder on its whole carrier. The Connected Ancestor Condition holds because two ancestors of z are both pred-iterates of z (exists_pred_iterate_of_le) and iterates are comparable (le_total_of_directed). B&P's structure is strictly more general (dense dominance orders have no PredOrder); this bridge realizes the general-plus-specialization pattern by construction.

Equations

• Core.Order.TreeOrder.ofPredArchimedean α = { nodes := Set.univ, root := ⊥, root_in_nodes := ⋯, root_le_all := ⋯, ancestor_connected := ⋯ }