Unordered rooted trees

An unordered rooted tree with vertices labelled in α is a RoseTree α modulo the permutation of children at every vertex: the quotient UnorderedTree α := Quotient RoseTree.isSetoid. In the Connes–Kreimer literature these are the rooted trees and the ordered ones the planar rooted trees ([Foi]); [marcolli-chomsky-berwick-2025] §1.1.3 builds syntactic objects on them, since Merge is set formation and {α, {β, γ}} has no order. The identity criterion is RoseTree.Perm (Core/Data/RoseTree/Perm.lean); this file owns the quotient: the projection mk, the lifting API, the lifted invariants, and the constructor node on Multiset children, under which the grafting B⁺ of a multiset of trees is well defined.

Main definitions

• UnorderedTree, UnorderedTree.mk: the quotient and its projection; operations descend through Quotient.lift and proofs through Quotient.inductionOn, as for Multiset.
• UnorderedTree.cons: adjoin a tree as a further child of the root, the transport of the list cons on children; it is left-commutative, so Multiset.foldr builds the constructor UnorderedTree.node on a multiset of children computably.

References

• [M. Marcolli, N. Chomsky and R. C. Berwick, Mathematical Structure of Syntactic Merge (2025)][marcolli-chomsky-berwick-2025]
• L. Foissy, An introduction to Hopf algebras of trees

The quotient type

def UnorderedTree (α : Type u_1) : Type u_1

An unordered rooted tree with α-labelled vertices: the quotient of RoseTree α by the permutation of children at every vertex, RoseTree.Perm.

Equations

• UnorderedTree α = Quotient RoseTree.isSetoid

def UnorderedTree.mk {α : Type u_1} (t : RoseTree α) : UnorderedTree α

The canonical projection from ordered to nonplanar trees.

Equations

• UnorderedTree.mk t = ⟦t⟧

theorem UnorderedTree.mk_eq_mk_iff {α : Type u_1} {t s : RoseTree α} : mk t = mk s ↔ t.Perm s

Two trees give the same nonplanar tree iff they're RoseTree.Perm-related.

@[simp]

theorem UnorderedTree.quot_mk_eq_mk {α : Type u_1} (t : RoseTree α) : ⟦t⟧ = mk t

The quotient projection in mk-form, so that goals produced by Quotient.inductionOn display mk and the mk-stated lemmas rewrite.

Smart leaf constructor + lifted counts

A leaf in UnorderedTree α is mk (RoseTree.leaf a). numNodes is the canonical first lifted invariant.

@[reducible, inline]

abbrev UnorderedTree.leaf {α : Type u_1} (a : α) : UnorderedTree α

A nonplanar leaf labeled a.

Equations

• UnorderedTree.leaf a = UnorderedTree.mk (RoseTree.leaf a)

def UnorderedTree.numNodes {α : Type u_1} : UnorderedTree α → ℕ

The node count (number of vertices) of a nonplanar tree, lifted from RoseTree.numNodes via RoseTree.Perm-invariance.

Equations

• UnorderedTree.numNodes = Quotient.lift RoseTree.numNodes ⋯

@[simp]

theorem UnorderedTree.numNodes_mk {α : Type u_1} (t : RoseTree α) : (mk t).numNodes = t.numNodes

@[simp]

theorem UnorderedTree.numNodes_leaf {α : Type u_1} (a : α) : (leaf a).numNodes = 1

def UnorderedTree.numLeaves {α : Type u_1} : UnorderedTree α → ℕ

The leaf count (number of childless vertices) of a nonplanar tree, lifted from RoseTree.numLeaves via RoseTree.Perm-invariance. MCB's complexity grading #L (Def. 1.6.2) is built on this.

Equations

• UnorderedTree.numLeaves = Quotient.lift RoseTree.numLeaves ⋯

@[simp]

theorem UnorderedTree.numLeaves_mk {α : Type u_1} (t : RoseTree α) : (mk t).numLeaves = t.numLeaves

@[simp]

theorem UnorderedTree.numLeaves_leaf {α : Type u_1} (a : α) : (leaf a).numLeaves = 1

def UnorderedTree.arity {α : Type u_1} : UnorderedTree α → ℕ

The arity (root child count) of a nonplanar tree.

Equations

• UnorderedTree.arity = Quotient.lift RoseTree.arity ⋯

@[simp]

theorem UnorderedTree.arity_mk {α : Type u_1} (t : RoseTree α) : (mk t).arity = t.arity

@[simp]

theorem UnorderedTree.arity_leaf {α : Type u_1} (a : α) : (leaf a).arity = 0

def UnorderedTree.height {α : Type u_1} : UnorderedTree α → ℕ

The height (number of vertices on a longest root-to-leaf path) of a nonplanar tree.

Equations

• UnorderedTree.height = Quotient.lift RoseTree.height ⋯

@[simp]

theorem UnorderedTree.height_mk {α : Type u_1} (t : RoseTree α) : (mk t).height = t.height

@[simp]

theorem UnorderedTree.height_leaf {α : Type u_1} (a : α) : (leaf a).height = 1

Destructors and node injectivity

The root value and the children (as a multiset of nonplanar trees) are RoseTree.Perm-invariant, so they descend to UnorderedTree. congrArg on these destructors inverts mk-equality at a node with no induction, giving the injectivity characterization mk_node_eq_mk_node_iff.

def UnorderedTree.value {α : Type u_1} : UnorderedTree α → α

The root value of a nonplanar tree.

Equations

• UnorderedTree.value = Quotient.lift RoseTree.value ⋯

@[simp]

theorem UnorderedTree.value_mk {α : Type u_1} (t : RoseTree α) : (mk t).value = t.value

theorem UnorderedTree.perm_children_map_mk {α : Type u_1} {t s : RoseTree α} (h : t.Perm s) : ↑(List.map mk t.children) = ↑(List.map mk s.children)

The mk-image of the root children, as a multiset, is a RoseTree.Perm-invariant: Perm.children_rel collapses under mk.

def UnorderedTree.children {α : Type u_1} : UnorderedTree α → Multiset (UnorderedTree α)

The children of a nonplanar tree, as a multiset of nonplanar trees.

Equations

• UnorderedTree.children = Quotient.lift (fun (t : RoseTree α) => ↑(List.map UnorderedTree.mk t.children)) ⋯

@[simp]

theorem UnorderedTree.children_mk {α : Type u_1} (t : RoseTree α) : (mk t).children = ↑(List.map mk t.children)

theorem UnorderedTree.mk_node_eq_mk_node_iff {α : Type u_1} {a b : α} {cs ds : List (RoseTree α)} : mk (RoseTree.node a cs) = mk (RoseTree.node b ds) ↔ a = b ∧ ↑(List.map mk cs) = ↑(List.map mk ds)

Injectivity of the node constructor on the quotient: mk-images of two nodes are equal iff the root values agree and the children agree as multisets of nonplanar trees. The forward direction is congrArg on the value and children destructors; the backward direction assembles a RoseTree.Perm componentwise.

Adjoining a child, and the node constructor

cons c t adjoins c as a further child of the root of t; it is the transport of the list cons on children lists and is left-commutative, so node a F is its Multiset.foldr over the children F starting from the leaf a. Both are computable, and node_mk_tree_list reads node back on a list of planar children.

def UnorderedTree.cons {α : Type u_1} (c t : UnorderedTree α) : UnorderedTree α

Adjoin a tree as a further child of the root.

Equations

• c.cons t = Quotient.liftOn₂ c t (fun (c t : RoseTree α) => UnorderedTree.mk (RoseTree.node t.value (c :: t.children))) ⋯

@[simp]

theorem UnorderedTree.cons_mk {α : Type u_1} (c : RoseTree α) (a : α) (cs : List (RoseTree α)) : (mk c).cons (mk (RoseTree.node a cs)) = mk (RoseTree.node a (c :: cs))

instance UnorderedTree.instLeftCommutativeCons {α : Type u_1} : LeftCommutative cons

def UnorderedTree.node {α : Type u_1} (a : α) (F : Multiset (UnorderedTree α)) : UnorderedTree α

Build an unordered tree from a label and a multiset of children, by adjoining the children one at a time to the leaf.

Equations

• UnorderedTree.node a F = Multiset.foldr UnorderedTree.cons (UnorderedTree.leaf a) F

@[simp]

theorem UnorderedTree.node_zero {α : Type u_1} (a : α) : node a 0 = leaf a

The empty-forest node is the leaf.

theorem UnorderedTree.node_cons {α : Type u_1} (a : α) (c : UnorderedTree α) (F : Multiset (UnorderedTree α)) : node a (c ::ₘ F) = c.cons (node a F)

@[simp]

theorem UnorderedTree.cons_node {α : Type u_1} (a : α) (c : UnorderedTree α) (F : Multiset (UnorderedTree α)) : c.cons (node a F) = node a (c ::ₘ F)

theorem UnorderedTree.node_mk_tree_list {α : Type u_1} (a : α) (ps : List (RoseTree α)) : node a ↑(List.map mk ps) = mk (RoseTree.node a ps)

node on the mk-image of a list of planar children is mk of the planar node.

theorem UnorderedTree.node_pair_mk {α : Type u_1} (a : α) (p q : RoseTree α) : node a {mk p, mk q} = mk (RoseTree.node a [p, q])

Binary case of node_mk_tree_list: a bare pair of mk-lifted trees.

theorem UnorderedTree.forest_inductionOn {α : Type u_1} {motive : Multiset (UnorderedTree α) → Prop} (F : Multiset (UnorderedTree α)) (h : ∀ (cs : List (RoseTree α)), motive ↑(List.map mk cs)) : motive F

Choose planar representatives for a whole forest at once: every Multiset (UnorderedTree α) is the mk-image of a list of planar trees. Descent proofs that use this eliminator meet node_mk_tree_list on the nose, with no Quotient.out repair.

The destructors of a node

@[simp]

theorem UnorderedTree.value_node {α : Type u_1} (a : α) (F : Multiset (UnorderedTree α)) : (node a F).value = a

@[simp]

theorem UnorderedTree.children_node {α : Type u_1} (a : α) (F : Multiset (UnorderedTree α)) : (node a F).children = F

theorem UnorderedTree.node_eta {α : Type u_1} (t : UnorderedTree α) : node t.value t.children = t

Eta law: every tree is the node of its root value and children.

Node count of a node

theorem UnorderedTree.numNodes_pos {α : Type u_1} (t : UnorderedTree α) : 0 < t.numNodes

Every tree has at least one vertex (the root).

@[simp]

theorem UnorderedTree.numNodes_node {α : Type u_1} (a : α) (F : Multiset (UnorderedTree α)) : (node a F).numNodes = (Multiset.map numNodes F).sum + 1

Node count of a smart-constructor node: one (the root) plus the total node count of the children multiset.

Height of a node

theorem UnorderedTree.height_lt_of_mem {α : Type u_1} (T : UnorderedTree α) (F : Multiset (UnorderedTree α)) (hT : T ∈ F) (a : α) : T.height < (node a F).height

A tree's height is strictly less than the height of any node containing it as a child.

Functoriality

Lift RoseTree.map through the quotient. Counterpart of List.map for lists: a function f : α → β lifts to UnorderedTree α → UnorderedTree β by relabeling every vertex.

def UnorderedTree.map {α : Type u_1} {β : Type u_2} (f : α → β) : UnorderedTree α → UnorderedTree β

Map a function over the vertex labels of a nonplanar rooted tree. Lifted from RoseTree.map via Quotient.map.

Equations

• UnorderedTree.map f = Quotient.map (RoseTree.map f) ⋯

theorem UnorderedTree.map_mk {α : Type u_1} {β : Type u_2} (f : α → β) (t : RoseTree α) : map f (mk t) = mk (RoseTree.map f t)

Quotient-unfolding for UnorderedTree.map. Plain lemma (not @[simp]) since mathlib's generic Quotient.map_mk covers the same ground.

theorem UnorderedTree.map_leaf {α : Type u_1} {β : Type u_2} (f : α → β) (a : α) : map f (leaf a) = leaf (f a)

@[simp]

theorem UnorderedTree.map_id {α : Type u_1} (t : UnorderedTree α) : map id t = t

theorem UnorderedTree.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : β → γ) (t : UnorderedTree α) : map g (map f t) = map (g ∘ f) t

theorem UnorderedTree.map_node {α : Type u_1} {β : Type u_2} (f : α → β) (a : α) (cs : Multiset (UnorderedTree α)) : map f (node a cs) = node (f a) (Multiset.map (map f) cs)

map commutes with node: relabel the root and map the children.

Counting interactions

@[simp]

theorem UnorderedTree.numNodes_map {α : Type u_1} {β : Type u_2} (f : α → β) (t : UnorderedTree α) : (map f t).numNodes = t.numNodes

@[simp]

theorem UnorderedTree.height_map {α : Type u_1} {β : Type u_2} (f : α → β) (t : UnorderedTree α) : (map f t).height = t.height

@[simp]

theorem UnorderedTree.arity_map {α : Type u_1} {β : Type u_2} (f : α → β) (t : UnorderedTree α) : (map f t).arity = t.arity

@[simp]

theorem UnorderedTree.numLeaves_map {α : Type u_1} {β : Type u_2} (f : α → β) (t : UnorderedTree α) : (map f t).numLeaves = t.numLeaves