Nonplanar n-ary rooted trees as a quotient of RoseTree α

[MCB25] [Foi]

A nonplanar rooted tree is a RoseTree α modulo the equivalence relation generated by:

• swapping two adjacent children of any vertex
• replacing a child with a nonplanar-equivalent tree (recursive step)

The quotient Nonplanar α := Quotient RoseTree.isSetoid gives the carrier MCB §1.1.2 + §1.10 actually wants for syntactic objects: trees with unordered children at each node.

Strategy

The identity criterion is RoseTree.Perm (Core/Data/RoseTree/Perm.lean), the List.Perm of trees; this file owns only the quotient: the projection mk, the lifting API, the lifted invariants, and the smart node constructor on Multiset-children. Invariance obligations are discharged by the relation's own theory (fold_perm, Perm.children_rel, the _perm invariants), never by a bespoke induction here.

Foissy connection

With Nonplanar α as carrier, B+_a : Multiset (Nonplanar α) → Nonplanar α becomes well-defined: graft the multiset of children under a new root labeled a. (For RoseTree α with multiset forests, B+ wasn't well-defined because the resulting tree's child-list ordering depended on choice of multiset representative.) This unblocks Foissy's clean cocycle proof of Δ^p coassoc on the nonplanar Hopf algebra (Phase A.7).

MCB anchor

[MCB25] §1.1.3 (book p. 20) — explicit caveat: {α, {β, γ}} = α △ β γ = α △ γ β = γ β △ α. This file's Nonplanar α realizes that unordered-children semantics for general arity.

Status

[UPSTREAM] candidate. No sorries.

Nonplanar — the quotient type

def RootedTree.Nonplanar (α : Type u_1) : Type u_1

A nonplanar n-ary rooted tree with α-labeled vertices: the quotient of RoseTree α by RoseTree.Perm.

Equations

• RootedTree.Nonplanar α = Quotient RoseTree.isSetoid

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

The canonical projection from ordered to nonplanar trees.

Equations

• RootedTree.Nonplanar.mk t = ⟦t⟧

theorem RootedTree.Nonplanar.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 RootedTree.Nonplanar.lift {α : Type u_1} {β : Sort u_2} (f : RoseTree α → β) (h : ∀ (t s : RoseTree α), t.Perm s → f t = f s) : Nonplanar α → β

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

Equations

• RootedTree.Nonplanar.lift f h = Quotient.lift f h

@[simp]

theorem RootedTree.Nonplanar.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 RootedTree.Nonplanar.inductionOn {α : Type u_1} {motive : Nonplanar α → Prop} (t : Nonplanar α) (mk : ∀ (p : RoseTree α), motive (mk p)) : motive t

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

theorem RootedTree.Nonplanar.inductionOn₂ {α : Type u_1} {motive : Nonplanar α → Nonplanar α → Prop} (t s : Nonplanar α) (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 Nonplanar α is mk (RoseTree.leaf a). numNodes is the canonical first lifted invariant.

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

A nonplanar leaf labeled a.

Equations

• RootedTree.Nonplanar.leaf a = RootedTree.Nonplanar.mk (RoseTree.leaf a)

@[simp]

theorem RootedTree.Nonplanar.leaf_def {α : Type u_1} (a : α) : leaf a = mk (RoseTree.leaf a)

def RootedTree.Nonplanar.numNodes {α : Type u_1} : Nonplanar α → ℕ

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

Equations

• RootedTree.Nonplanar.numNodes = RootedTree.Nonplanar.lift RoseTree.numNodes ⋯

@[simp]

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

@[simp]

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

def RootedTree.Nonplanar.numLeaves {α : Type u_1} : Nonplanar α → ℕ

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

• RootedTree.Nonplanar.numLeaves = RootedTree.Nonplanar.lift RoseTree.numLeaves ⋯

@[simp]

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

@[simp]

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

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

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

Equations

• RootedTree.Nonplanar.arity = RootedTree.Nonplanar.lift RoseTree.arity ⋯

@[simp]

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

@[simp]

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

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

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

Equations

• RootedTree.Nonplanar.depth = RootedTree.Nonplanar.lift RoseTree.depth ⋯

@[simp]

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

@[simp]

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

def RootedTree.Nonplanar.isLeaf {α : Type u_1} : Nonplanar α → 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

• RootedTree.Nonplanar.isLeaf = RootedTree.Nonplanar.lift RoseTree.isLeaf ⋯

@[simp]

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

@[simp]

theorem RootedTree.Nonplanar.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 Nonplanar. congrArg on these destructors inverts mk-equality at a node with no induction, giving the injectivity characterization mk_node_eq_mk_node_iff.

def RootedTree.Nonplanar.value {α : Type u_1} : Nonplanar α → α

The root value of a nonplanar tree.

Equations

• RootedTree.Nonplanar.value = RootedTree.Nonplanar.lift RoseTree.value ⋯

@[simp]

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

theorem RootedTree.Nonplanar.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 RootedTree.Nonplanar.children {α : Type u_1} : Nonplanar α → Multiset (Nonplanar α)

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

Equations

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

@[simp]

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

theorem RootedTree.Nonplanar.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 Nonplanar α from a label and an unordered collection of children. The smart constructor node a cs does this on Multiset (Nonplanar α); 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 RootedTree.Nonplanar.node {α : Type u_1} (a : α) (cs : Multiset (Nonplanar α)) : Nonplanar α

Build a Nonplanar α 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

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

theorem RootedTree.Nonplanar.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 Nonplanar α from a list of tree children (lifted to nonplanar via mk) agrees with directly lifting the tree node a ps.

theorem RootedTree.Nonplanar.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 RootedTree.Nonplanar.forest_inductionOn {α : Type u_1} {motive : Multiset (Nonplanar α) → Prop} (F : Multiset (Nonplanar α)) (h : ∀ (cs : List (RoseTree α)), motive ↑(List.map mk cs)) : motive F

Choose planar representatives for a whole forest at once: every Multiset (Nonplanar α) 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 RootedTree.Nonplanar.rootValue {α : Type u_1} : Nonplanar α → α

The root value of a nonplanar tree.

Equations

• RootedTree.Nonplanar.rootValue = RootedTree.Nonplanar.lift RoseTree.value ⋯

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

The multiset of root children of a nonplanar tree.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem RootedTree.Nonplanar.node_eta {α : Type u_1} (t : Nonplanar α) : 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 RootedTree.Nonplanar.numNodes_pos {α : Type u_1} (t : Nonplanar α) : 0 < t.numNodes

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

@[simp]

theorem RootedTree.Nonplanar.numNodes_node {α : Type u_1} (a : α) (F : Multiset (Nonplanar α)) : (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.

Functoriality

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

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

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

Equations

• RootedTree.Nonplanar.map f = Quotient.map (RoseTree.map f) ⋯

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

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

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

@[simp]

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

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

Counting interactions

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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