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

[MCB25] [foissy-introduction-hopf-algebras-trees]

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.instSetoid gives the carrier MCB §1.1.2 + §1.10 actually wants for syntactic objects: trees with unordered children at each node.

Strategy

Define a primitive PermStep relation that captures a single elementary move (a swap or a recursive substitution), then take the equivalence closure via Relation.EqvGen. This way:

• The equivalence relation IS automatically an equivalence (via the reflexive/symmetric/transitive constructors of EqvGen).
• Proving things about it reduces to handling the elementary PermStep cases plus the equivalence-closure constructors.

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.

PermStep — elementary moves

A PermStep t s says: s is obtained from t by either:

• swapping two adjacent children of some vertex, or
• replacing a single child with a tree related by PermStep (recursion).

inductive RoseTree.PermStep {α : Type u_1} : RoseTree α → RoseTree α → Prop

A single-step child-permutation move on a rooted tree.

• swapAtRoot {α : Type u_1} {a : α} {l r : RoseTree α} {pre post : List (RoseTree α)} : (node a (pre ++ l :: r :: post)).PermStep (node a (pre ++ r :: l :: post))

  Swap two adjacent children at the root vertex.

• recurse {α : Type u_1} {a : α} {pre : List (RoseTree α)} {old new : RoseTree α} {post : List (RoseTree α)} (h : old.PermStep new) : (node a (pre ++ old :: post)).PermStep (node a (pre ++ new :: post))

  Apply a step inside a child subtree, leaving siblings unchanged.

PermEquiv — equivalence closure

The nonplanar-equivalence relation on trees: the equivalence closure of PermStep. Built using Relation.EqvGen, so it's automatically reflexive / symmetric / transitive.

def RoseTree.PermEquiv {α : Type u_1} : RoseTree α → RoseTree α → Prop

Nonplanar equivalence on trees: equivalence closure of PermStep.

Equations

• RoseTree.PermEquiv = Relation.EqvGen RoseTree.PermStep

theorem RoseTree.PermEquiv.refl {α : Type u_1} (t : RoseTree α) : t.PermEquiv t

theorem RoseTree.PermEquiv.symm {α : Type u_1} {t s : RoseTree α} (h : t.PermEquiv s) : s.PermEquiv t

theorem RoseTree.PermEquiv.trans {α : Type u_1} {t s u : RoseTree α} (h₁ : t.PermEquiv s) (h₂ : s.PermEquiv u) : t.PermEquiv u

theorem RoseTree.PermEquiv.of_step {α : Type u_1} {t s : RoseTree α} (h : t.PermStep s) : t.PermEquiv s

theorem RoseTree.PermEquiv.isEquivalence {α : Type u_1} : Equivalence PermEquiv

Lifting structural invariants from RoseTree to Nonplanar

Functions RoseTree α → β that are invariant under PermStep lift through the equivalence closure to functions Nonplanar α → β. Below we lift numNodes (vertex count) and the other counts as worked examples.

The pattern: prove invariance under the elementary PermStep, then extend to PermEquiv = EqvGen PermStep by an EqvGen induction. On RoseTree the counts sum/foldr-max directly over cs.map …, so permutation invariance is just List.Perm.sum_eq / List.Perm.foldr_eq on the child list.

Node count invariance

theorem RoseTree.numNodes_permEquiv {α : Type u_1} {t s : RoseTree α} (h : t.PermEquiv s) : t.numNodes = s.numNodes

numNodes is invariant under PermEquiv. By induction on EqvGen.

Leaf-count invariance

theorem RoseTree.numLeaves_permEquiv {α : Type u_1} {t s : RoseTree α} (h : t.PermEquiv s) : t.numLeaves = s.numLeaves

numLeaves is invariant under PermEquiv.

Value invariance

theorem RoseTree.value_permEquiv {α : Type u_1} {t s : RoseTree α} (h : t.PermEquiv s) : t.value = s.value

The root value is preserved by PermEquiv.

Lifting child-list operations to PermEquiv

The smart constructor Nonplanar.node needs to know that the parent-node equivalence respects the natural list-of-children operations: cons (sibling-prepend), permutation, and componentwise equivalence.

theorem RoseTree.permEquiv_recurse_lift {α : Type u_1} {a : α} (pre post : List (RoseTree α)) {old new : RoseTree α} (h : old.PermEquiv new) : (node a (pre ++ old :: post)).PermEquiv (node a (pre ++ new :: post))

Lift a PermEquiv from a child to the parent that has identical pre- and post-siblings (a chain of recurse moves).

theorem RoseTree.permEquiv_cons_lift {α : Type u_1} (x : RoseTree α) {a : α} {cs ds : List (RoseTree α)} (h : (node a cs).PermEquiv (node a ds)) : (node a (x :: cs)).PermEquiv (node a (x :: ds))

A PermEquiv between root nodes lifts under a sibling-cons.

theorem RoseTree.permEquiv_root_perm {α : Type u_1} {a : α} {cs ds : List (RoseTree α)} (h : cs.Perm ds) : (node a cs).PermEquiv (node a ds)

A List.Perm at root level lifts to PermEquiv on the node.

theorem RoseTree.permEquiv_node_componentwise {α : Type u_1} {a : α} {cs ds : List (RoseTree α)} (h : List.Forall₂ PermEquiv cs ds) : (node a cs).PermEquiv (node a ds)

A componentwise PermEquiv on root children lifts to PermEquiv on the node.

Arity / depth / isLeaf invariance

Three more invariants of tree structure that are preserved by PermEquiv. The pattern follows numNodes: prove *_permStep by case on the step constructor, then lift to *_permEquiv via EqvGen induction.

theorem RoseTree.arity_permEquiv {α : Type u_1} {t s : RoseTree α} (h : t.PermEquiv s) : t.arity = s.arity

Arity is invariant under PermEquiv.

theorem RoseTree.depth_permEquiv {α : Type u_1} {t s : RoseTree α} (h : t.PermEquiv s) : t.depth = s.depth

Depth is invariant under PermEquiv.

theorem RoseTree.isLeaf_permEquiv {α : Type u_1} {t s : RoseTree α} (h : t.PermEquiv s) : t.isLeaf = s.isLeaf

Leaf-ness is invariant under PermEquiv.

Setoid instance

@[implicit_reducible]

instance RoseTree.instSetoid {α : Type u_1} : Setoid (RoseTree α)

The setoid on RoseTree α whose quotient is Nonplanar α.

Equations

• RoseTree.instSetoid = { r := RoseTree.PermEquiv, iseqv := ⋯ }

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 PermEquiv.

Equations

• RootedTree.Nonplanar α = Quotient RoseTree.instSetoid

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.PermEquiv s

Two trees give the same nonplanar tree iff they're PermEquiv.

@[simp]

theorem RootedTree.Nonplanar.mk_step {α : Type u_1} {t s : RoseTree α} (h : t.PermStep s) : mk t = mk s

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

Lift a function RoseTree α → β that's invariant under PermEquiv 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.PermEquiv s → f t = f s) (t : RoseTree α) : lift f h (mk t) = f t

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 PermEquiv-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 PermEquiv-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 PermEquiv-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

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 PermEquiv 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.permEquiv_root_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.

Sanity tests

Root value and children

Root-level projections, lifted through the quotient: RoseTree.value is PermEquiv-invariant on the nose (value_permEquiv), and the mk-image of RoseTree.children is invariant as a multiset (root swaps permute the list; recursive steps rewrite a child within its mk-class).

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

The mk-image of the root children, as a multiset, is preserved by PermEquiv.

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 of map under PermEquiv

Setup for Nonplanar.map: lift RoseTree.map through the quotient by showing it preserves the equivalence relation. Done in two steps: elementary PermStep preservation, then closure under EqvGen.

theorem RoseTree.permEquiv_map {α : Type u_1} {β : Type u_2} (f : α → β) {t s : RoseTree α} (h : t.PermEquiv s) : (map f t).PermEquiv (map f s)

RoseTree.map preserves PermEquiv (the equivalence closure of PermStep). Substrate for Nonplanar.map.

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