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

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

A nonplanar rooted tree is a Planar α 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 PlanarSetoid 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 Step 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 Step 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 Planar α 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

@cite{marcolli-chomsky-berwick-2025} §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.

PlanarStep — elementary moves

A PlanarStep 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 PlanarStep (recursion).

inductive RootedTree.Planar.PlanarStep {α : Type u_1} : Planar α → Planar α → Prop

A single-step nonplanar permutation move on a planar tree.

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

  Swap two adjacent children at the root vertex.

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

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

PlanarEquiv — equivalence closure

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

def RootedTree.Planar.PlanarEquiv {α : Type u_1} : Planar α → Planar α → Prop

Nonplanar equivalence on planar trees: equivalence closure of PlanarStep.

Equations

• RootedTree.Planar.PlanarEquiv = Relation.EqvGen RootedTree.Planar.PlanarStep

theorem RootedTree.Planar.PlanarEquiv.refl {α : Type u_1} (t : Planar α) : t.PlanarEquiv t

theorem RootedTree.Planar.PlanarEquiv.symm {α : Type u_1} {t s : Planar α} (h : t.PlanarEquiv s) : s.PlanarEquiv t

theorem RootedTree.Planar.PlanarEquiv.trans {α : Type u_1} {t s u : Planar α} (h₁ : t.PlanarEquiv s) (h₂ : s.PlanarEquiv u) : t.PlanarEquiv u

theorem RootedTree.Planar.PlanarEquiv.of_step {α : Type u_1} {t s : Planar α} (h : t.PlanarStep s) : t.PlanarEquiv s

theorem RootedTree.Planar.PlanarEquiv.isEquivalence {α : Type u_1} : Equivalence PlanarEquiv

Lifting structural invariants from Planar to Nonplanar

Functions Planar α → β that are invariant under PlanarStep lift through the equivalence closure to functions Nonplanar α → β. Below we lift weight (vertex count) and arity-at-root as worked examples.

The pattern: prove invariance under the elementary PlanarStep, then extend to PlanarEquiv = EqvGen PlanarStep by an EqvGen induction.

Weight invariance

theorem RootedTree.Planar.weight_planarEquiv {α : Type u_1} {t s : Planar α} (h : t.PlanarEquiv s) : t.weight = s.weight

Weight is invariant under PlanarEquiv. By induction on EqvGen.

Label invariance

theorem RootedTree.Planar.planarEquiv_label_eq {α : Type u_1} {t s : Planar α} (h : t.PlanarEquiv s) : t.label = s.label

The root label is preserved by PlanarEquiv.

Lifting child-list operations to PlanarEquiv

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 RootedTree.Planar.planarEquiv_recurse_lift {α : Type u_1} {a : α} (pre post : List (Planar α)) {old new : Planar α} (h : old.PlanarEquiv new) : (node a (pre ++ old :: post)).PlanarEquiv (node a (pre ++ new :: post))

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

theorem RootedTree.Planar.planarEquiv_cons_lift {α : Type u_1} (x : Planar α) {a : α} {cs ds : List (Planar α)} (h : (node a cs).PlanarEquiv (node a ds)) : (node a (x :: cs)).PlanarEquiv (node a (x :: ds))

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

theorem RootedTree.Planar.planarEquiv_root_perm {α : Type u_1} {a : α} {cs ds : List (Planar α)} (h : cs.Perm ds) : (node a cs).PlanarEquiv (node a ds)

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

theorem RootedTree.Planar.planarEquiv_node_componentwise {α : Type u_1} {a : α} {cs ds : List (Planar α)} (h : List.Forall₂ PlanarEquiv cs ds) : (node a cs).PlanarEquiv (node a ds)

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

Arity / depth / isLeaf invariance

Three more invariants of tree structure that are preserved by PlanarEquiv. The pattern follows weight (§3a): prove *_planarStep by case on the step constructor (using a per-list permutation lemma when the function aggregates over children), then lift to *_planarEquiv via EqvGen induction.

theorem RootedTree.Planar.arity_planarEquiv {α : Type u_1} {t s : Planar α} (h : t.PlanarEquiv s) : t.arity = s.arity

Arity is invariant under PlanarEquiv.

theorem RootedTree.Planar.depth_planarEquiv {α : Type u_1} {t s : Planar α} (h : t.PlanarEquiv s) : t.depth = s.depth

Depth is invariant under PlanarEquiv.

theorem RootedTree.Planar.isLeaf_planarEquiv {α : Type u_1} {t s : Planar α} (h : t.PlanarEquiv s) : t.isLeaf = s.isLeaf

Leaf-ness is invariant under PlanarEquiv.

Setoid instance

@[implicit_reducible]

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

The setoid on Planar α whose quotient is Nonplanar α.

Equations

• RootedTree.Planar.instSetoid = { r := RootedTree.Planar.PlanarEquiv, 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 Planar α by PlanarEquiv.

Equations

• RootedTree.Nonplanar α = Quotient RootedTree.Planar.instSetoid

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

The canonical projection from planar to nonplanar trees.

Equations

• RootedTree.Nonplanar.mk t = ⟦t⟧

theorem RootedTree.Nonplanar.mk_eq_mk_iff {α : Type u_1} {t s : Planar α} : mk t = mk s ↔ t.PlanarEquiv s

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

@[simp]

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

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

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

Smart leaf constructor + lifted weight

A leaf in Nonplanar α is mk (Planar.leaf a). Weight 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 (RootedTree.Planar.leaf a)

@[simp]

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

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

The weight (vertex count) of a nonplanar tree, lifted from Planar.weight via PlanarEquiv-invariance.

Equations

• RootedTree.Nonplanar.weight = RootedTree.Nonplanar.lift RootedTree.Planar.weight ⋯

@[simp]

theorem RootedTree.Nonplanar.weight_mk {α : Type u_1} (t : Planar α) : (mk t).weight = t.weight

@[simp]

theorem RootedTree.Nonplanar.weight_leaf {α : Type u_1} (a : α) : (leaf a).weight = 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 RootedTree.Planar.arity ⋯

@[simp]

theorem RootedTree.Nonplanar.arity_mk {α : Type u_1} (t : Planar α) : (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) of a nonplanar tree.

Equations

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

@[simp]

theorem RootedTree.Nonplanar.depth_mk {α : Type u_1} (t : Planar α) : (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 Planar.isLeaf is migrated.)

Equations

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

@[simp]

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

@[simp]

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

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 Planar.planarEquiv_root_perm (children-list permutation invariance). The characterization node_mk_planar_list then bridges back to the underlying planar 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 planar representatives via Quotient.out, and quotient back.

Equations

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

theorem RootedTree.Nonplanar.node_mk_planar_list {α : Type u_1} (a : α) (ps : List (Planar α)) : node a ↑(List.map mk ps) = mk (Planar.node a ps)

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

Sanity tests

Functoriality of map under PlanarEquiv

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

theorem RootedTree.Planar.planarEquiv_map {α : Type u_1} {β : Type u_2} (f : α → β) {t s : Planar α} (h : t.PlanarEquiv s) : (map f t).PlanarEquiv (map f s)

Planar.map preserves PlanarEquiv (the equivalence closure of PlanarStep). Substrate for Nonplanar.map.

Functoriality

Lift Planar.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 Planar.map via Quotient.map.

Equations

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

theorem RootedTree.Nonplanar.map_mk {α : Type u_1} {β : Type u_2} (f : α → β) (t : Planar α) : map f (mk t) = mk (Planar.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.weight_map {α : Type u_1} {β : Type u_2} (f : α → β) (t : Nonplanar α) : (map f t).weight = t.weight

@[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