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, UnorderedTree.lift, UnorderedTree.node

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.

def UnorderedTree.lift {α : Type u_1} {β : Sort u_2} (f : RoseTree α → β) (h : ∀ (t s : RoseTree α), t.Perm s → f t = f s) : UnorderedTree α → β

Lift a function RoseTree α → β that's invariant under RoseTree.Perm to UnorderedTree α → β.

Equations

• UnorderedTree.lift f h = Quotient.lift f h

@[simp]

theorem UnorderedTree.lift_mk {α : Type u_1} {β : Sort u_2} (f : RoseTree α → β) (h : ∀ (t s : RoseTree α), t.Perm s → f t = f s) (t : RoseTree α) : lift f h (mk t) = f t

theorem UnorderedTree.inductionOn {α : Type u_1} {motive : UnorderedTree α → Prop} (t : UnorderedTree α) (mk : ∀ (p : RoseTree α), motive (mk p)) : motive t

Induction in mk-form (cf. Multiset.induction_on): goals display UnorderedTree.mk rather than Quotient.mk, so mk-stated lemmas rewrite.

theorem UnorderedTree.inductionOn₂ {α : Type u_1} {motive : UnorderedTree α → UnorderedTree α → Prop} (t s : UnorderedTree α) (mk : ∀ (p q : RoseTree α), motive (mk p) (mk q)) : motive t s

Binary induction in mk-form.

Smart leaf constructor + lifted counts

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

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

A nonplanar leaf labeled a.

Equations

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

@[simp]

theorem UnorderedTree.leaf_def {α : Type u_1} (a : α) : leaf a = 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 = UnorderedTree.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 = UnorderedTree.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 = UnorderedTree.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.depth {α : Type u_1} : UnorderedTree α → ℕ

The depth (longest root-to-leaf path in vertices) of a nonplanar tree.

Equations

• UnorderedTree.depth = UnorderedTree.lift RoseTree.depth ⋯

@[simp]

theorem UnorderedTree.depth_mk {α : Type u_1} (t : RoseTree α) : (mk t).depth = t.depth

@[simp]

theorem UnorderedTree.depth_leaf {α : Type u_1} (a : α) : (leaf a).depth = 1

def UnorderedTree.isLeaf {α : Type u_1} : UnorderedTree α → Bool

A nonplanar tree is a leaf if its root has no children. (Audit item: queue migrate to Prop + [DecidablePred] once the matching RoseTree.isLeaf is migrated.)

Equations

• UnorderedTree.isLeaf = UnorderedTree.lift RoseTree.isLeaf ⋯

@[simp]

theorem UnorderedTree.isLeaf_mk {α : Type u_1} (t : RoseTree α) : (mk t).isLeaf = t.isLeaf

@[simp]

theorem UnorderedTree.isLeaf_leaf {α : Type u_1} (a : α) : (leaf a).isLeaf = true

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 = UnorderedTree.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 = UnorderedTree.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.

Smart node constructor

The B+ operator (Phase A.7) and the Δ^c trace coproduct (Phase D) both require building a UnorderedTree α from a label and an unordered collection of children. The smart constructor node a cs does this on Multiset (UnorderedTree α); well-definedness follows from RoseTree.Perm.node_of_perm (children-list permutation invariance). The characterization node_mk_tree_list then bridges back to the underlying RoseTree node via Quotient.mk_out componentwise.

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

Build a UnorderedTree α from a label and an unordered multiset of children. Implementation: pick a list representative of the multiset (Quotient.liftOn), then per-child tree representatives via Quotient.out, and quotient back.

Equations

• UnorderedTree.node a cs = Quotient.liftOn cs (fun (lst : List (UnorderedTree α)) => UnorderedTree.mk (RoseTree.node a (List.map Quotient.out lst))) ⋯

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

Characterization: building a UnorderedTree α from a list of tree children (lifted to nonplanar via mk) agrees with directly lifting the tree node a ps.

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.

@[simp]

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

The empty-forest node is the leaf.

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.

Sanity tests

Root value and children

Root-level projections, lifted through the quotient: RoseTree.value is RoseTree.Perm-invariant on the nose (Perm.value_eq), and the mk-image of RoseTree.children is invariant as a multiset (perm_children_map_mk).

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

The root value of a nonplanar tree.

Equations

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

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

The multiset of root children of a nonplanar tree.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem UnorderedTree.node_eta {α : Type u_1} (t : UnorderedTree α) : node t.rootValue t.rootChildren = t

Eta law: every tree is the node of its root value and root 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 = 1 + (Multiset.map numNodes F).sum

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

Depth of a node

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

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

Edge count of a forest

def UnorderedTree.Forest.edgeCount {α : Type u_1} (F : Multiset (UnorderedTree α)) : ℕ

Total edge count of a forest of nonplanar trees: each tree with n vertices contributes n - 1 edges. Defined as a per-tree sum (no global subtraction) so additivity is immediate.

Equations

• UnorderedTree.Forest.edgeCount F = (Multiset.map (fun (T : UnorderedTree α) => T.numNodes - 1) F).sum

@[simp]

theorem UnorderedTree.Forest.edgeCount_zero {α : Type u_1} : edgeCount 0 = 0

@[simp]

theorem UnorderedTree.Forest.edgeCount_singleton {α : Type u_1} (T : UnorderedTree α) : edgeCount {T} = T.numNodes - 1

@[simp]

theorem UnorderedTree.Forest.edgeCount_cons {α : Type u_1} (T : UnorderedTree α) (F : Multiset (UnorderedTree α)) : edgeCount (T ::ₘ F) = T.numNodes - 1 + edgeCount F

@[simp]

theorem UnorderedTree.Forest.edgeCount_add {α : Type u_1} (F G : Multiset (UnorderedTree α)) : edgeCount (F + G) = edgeCount F + edgeCount G

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.depth_map {α : Type u_1} {β : Type u_2} (f : α → β) (t : UnorderedTree α) : (map f t).depth = t.depth

@[simp]

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

@[simp]

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

@[simp]

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