Planar n-ary rooted trees with vertex labels in α

@cite{marcolli-chomsky-berwick-2025} @cite{foissy-introduction-hopf-algebras-trees}

A planar rooted tree has: a distinguished root vertex, an α-label at every vertex, and an ordered (list-valued) sequence of children at each non-leaf vertex. Each vertex's "arity" is the length of its child list; leaves are vertices with empty child lists. There is no global arity bound — vertices may have any number of children.

This is the most general planar tree carrier the Connes-Kreimer-style Hopf algebra needs. Specializations as subtypes:

• Binary (every internal vertex has exactly 2 children) ≃ FreeMagma α (the existing linglib binary planar carrier).
• NaryAtMost n (every vertex has ≤ n children).
• NaryExactly n (every internal vertex has exactly n children, leaves 0).

The nonplanar version (children as multiset, not list) is in RootedTree.Nonplanar (sibling file), defined as a quotient by permutations of children at each level.

Why list-of-children, not multiset directly

Lean 4's strict positivity check rejects inductive Tree | node : α → Multiset (Tree α) → Tree α because Multiset = Quot (List _) _ is opaque to the positivity checker. The standard workaround: define the planar (list-valued) version as a genuine inductive, then quotient by a permutation relation to get the nonplanar version. This file provides the list-valued primitive; Nonplanar.lean provides the quotient.

MCB anchor

@cite{marcolli-chomsky-berwick-2025} §1.11 introduces n-ary syntactic objects SO^(n) ≃ ℑ^(n)_{SO_0} as the free nonassociative commutative n-magma; book p. 96 Definition 1.11.2. §1.17 uses the n-ary Connes-Kreimer Hopf algebra of rooted trees in the recursive construction of solutions to combinatorial Dyson-Schwinger equations (book p. 149-150). The carrier here is parameterized over arity (no fixed n), subsuming all n-ary cases via subtypes.

@cite{foissy-introduction-hopf-algebras-trees} §1.1 (p. 3) introduces rooted trees as finite graphs, connected and without cycles, with a distinguished root vertex; this file's Planar is the planar / ordered variant (Foissy's H_PR setting, §2). The nonplanar variant (Foissy's H_R, §1) is the quotient in Nonplanar.lean.

Status

[UPSTREAM] candidate; future home something like Mathlib.Combinatorics.RootedTree.Planar. No sorries, no noncomputable, no decide in this file.

§1: The Planar inductive

A planar rooted tree is built by node a cs where a : α is the root label and cs : List (Planar α) is the ordered list of children. Leaves are node a [].

inductive RootedTree.Planar (α : Type u_1) : Type u_1

A planar rooted tree with α-labeled vertices and ordered children.

• node {α : Type u_1} (a : α) (cs : List (Planar α)) : Planar α

§2: Basic projections

def RootedTree.Planar.label {α : Type u_1} : Planar α → α

The label at the root vertex.

Equations

• (RootedTree.Planar.node a cs).label = a

def RootedTree.Planar.children {α : Type u_1} : Planar α → List (Planar α)

The (ordered) list of children at the root.

Equations

• (RootedTree.Planar.node a cs).children = cs

@[simp]

theorem RootedTree.Planar.label_node {α : Type u_1} (a : α) (cs : List (Planar α)) : (node a cs).label = a

@[simp]

theorem RootedTree.Planar.children_node {α : Type u_1} (a : α) (cs : List (Planar α)) : (node a cs).children = cs

§3: Counting — weight, arity, depth

Defined by structural recursion (mutual with the list-of-trees aux).

def RootedTree.Planar.weight {α : Type u_1} : Planar α → ℕ

The weight of a tree: total number of vertices.

Equations

• (RootedTree.Planar.node a cs).weight = 1 + RootedTree.Planar.weightList cs

def RootedTree.Planar.weightList {α : Type u_1} : List (Planar α) → ℕ

Auxiliary: total weight of a list of trees.

Equations

• RootedTree.Planar.weightList [] = 0
• RootedTree.Planar.weightList (t :: ts) = t.weight + RootedTree.Planar.weightList ts

def RootedTree.Planar.depth {α : Type u_1} : Planar α → ℕ

The depth of a tree: longest root-to-leaf path length (in edges). A leaf has depth 0.

Equations

• (RootedTree.Planar.node a cs).depth = 1 + RootedTree.Planar.depthMaxList cs

def RootedTree.Planar.depthMaxList {α : Type u_1} : List (Planar α) → ℕ

Auxiliary: max depth across a list of trees (0 for empty).

Equations

• RootedTree.Planar.depthMaxList [] = 0
• RootedTree.Planar.depthMaxList (t :: ts) = max t.depth (RootedTree.Planar.depthMaxList ts)

def RootedTree.Planar.arity {α : Type u_1} : Planar α → ℕ

The arity of the root vertex: number of children. Leaves have arity 0.

Equations

• (RootedTree.Planar.node a cs).arity = cs.length

def RootedTree.Planar.isLeaf {α : Type u_1} : Planar α → Bool

A tree is a leaf if its root has no children.

Equations

• (RootedTree.Planar.node a []).isLeaf = true
• (RootedTree.Planar.node a (head :: tail)).isLeaf = false

@[simp]

theorem RootedTree.Planar.arity_node {α : Type u_1} (a : α) (cs : List (Planar α)) : (node a cs).arity = cs.length

@[simp]

theorem RootedTree.Planar.isLeaf_node_nil {α : Type u_1} (a : α) : (node a []).isLeaf = true

@[simp]

theorem RootedTree.Planar.isLeaf_node_cons {α : Type u_1} (a : α) (c : Planar α) (cs : List (Planar α)) : (node a (c :: cs)).isLeaf = false

§4: Smart constructors

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

A leaf with the given α-label.

Equations

• RootedTree.Planar.leaf a = RootedTree.Planar.node a []

def RootedTree.Planar.unary {α : Type u_1} (a : α) (c : Planar α) : Planar α

A unary node: single child.

Equations

• RootedTree.Planar.unary a c = RootedTree.Planar.node a [c]

def RootedTree.Planar.binary {α : Type u_1} (a : α) (l r : Planar α) : Planar α

A binary node: two children, in left-to-right order.

Equations

• RootedTree.Planar.binary a l r = RootedTree.Planar.node a [l, r]

def RootedTree.Planar.nary {α : Type u_1} (a : α) (cs : List (Planar α)) : Planar α

An n-ary node: list of children.

Equations

• RootedTree.Planar.nary a cs = RootedTree.Planar.node a cs

@[simp]

theorem RootedTree.Planar.leaf_def {α : Type u_1} (a : α) : leaf a = node a []

@[simp]

theorem RootedTree.Planar.unary_def {α : Type u_1} (a : α) (c : Planar α) : unary a c = node a [c]

@[simp]

theorem RootedTree.Planar.binary_def {α : Type u_1} (a : α) (l r : Planar α) : binary a l r = node a [l, r]

@[simp]

theorem RootedTree.Planar.nary_def {α : Type u_1} (a : α) (cs : List (Planar α)) : nary a cs = node a cs

§5: Functoriality

Planar is a functor in the vertex-label parameter: a function f : α → β lifts to Planar α → Planar β by relabeling every vertex. Defined by mutual structural recursion on (tree, list-of-trees). Counterpart of mathlib's Tree.map for binary trees and List.map for lists.

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

Map a function over the vertex labels of a planar rooted tree.

Equations

• RootedTree.Planar.map f (RootedTree.Planar.node a cs) = RootedTree.Planar.node (f a) (RootedTree.Planar.mapList f cs)

def RootedTree.Planar.mapList {α : Type u_1} {β : Type u_2} (f : α → β) : List (Planar α) → List (Planar β)

Auxiliary: map across a list of children.

Equations

• RootedTree.Planar.mapList f [] = []
• RootedTree.Planar.mapList f (t :: ts) = RootedTree.Planar.map f t :: RootedTree.Planar.mapList f ts

@[simp]

theorem RootedTree.Planar.map_node {α : Type u_1} {β : Type u_2} (f : α → β) (a : α) (cs : List (Planar α)) : map f (node a cs) = node (f a) (mapList f cs)

@[simp]

theorem RootedTree.Planar.mapList_nil {α : Type u_1} {β : Type u_2} (f : α → β) : mapList f [] = []

@[simp]

theorem RootedTree.Planar.mapList_cons {α : Type u_1} {β : Type u_2} (f : α → β) (c : Planar α) (cs : List (Planar α)) : mapList f (c :: cs) = map f c :: mapList f cs

theorem RootedTree.Planar.mapList_eq_listMap {α : Type u_1} {β : Type u_2} (f : α → β) (cs : List (Planar α)) : mapList f cs = List.map (map f) cs

mapList f agrees with List.map (map f). Bridge to mathlib's List.map API.

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

map on a leaf. Provable by simp from leaf_def + map_node + mapList_nil, so kept as a plain rw lemma (no @[simp]) to avoid simp non-confluence.

@[simp]

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

Functoriality: map id = id.

@[simp]

theorem RootedTree.Planar.mapList_id {α : Type u_1} (cs : List (Planar α)) : mapList id cs = cs

@[simp]

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

Functoriality: map (g ∘ f) = map g ∘ map f.

@[simp]

theorem RootedTree.Planar.mapList_mapList {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : β → γ) (cs : List (Planar α)) : mapList g (mapList f cs) = mapList (g ∘ f) cs

Counting interactions

@[simp]

theorem RootedTree.Planar.weight_map {α : Type u_1} {β : Type u_2} (f : α → β) (t : Planar α) : (map f t).weight = t.weight

theorem RootedTree.Planar.weightList_mapList {α : Type u_1} {β : Type u_2} (f : α → β) (cs : List (Planar α)) : weightList (mapList f cs) = weightList cs

@[simp]

theorem RootedTree.Planar.depth_map {α : Type u_1} {β : Type u_2} (f : α → β) (t : Planar α) : (map f t).depth = t.depth

theorem RootedTree.Planar.depthMaxList_mapList {α : Type u_1} {β : Type u_2} (f : α → β) (cs : List (Planar α)) : depthMaxList (mapList f cs) = depthMaxList cs

@[simp]

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

@[simp]

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

§5b: Sanity tests at compile time

§6: Inhabited

@[implicit_reducible]

instance RootedTree.Planar.instInhabited {α : Type u_1} [Inhabited α] : Inhabited (Planar α)

Equations

• RootedTree.Planar.instInhabited = { default := RootedTree.Planar.leaf default }