Nonplanar multi-tree insertion

Lift of Planar.Pathed.insertionForest through Nonplanar.mk.

Given two multisets of nonplanar trees F (host forest) and G (guest forest), Nonplanar.insertionMultiset F G produces the multiset of all forests obtained by inserting G's trees at vertices of F's trees, summing over all assignments (Foissy 2021 Theorem 5.1).

Implementation note

The implementation uses Multiset.toList + Quotient.out to pick representatives, making it noncomputable. The function value is nonetheless well-defined (classical choice yields a definite element). Stronger invariance theorems (host-Perm invariance lifted to the multiset-output level) would enable a Quotient.liftOn₂-based definition but are deferred — the current API suffices for the GrossmanLarson product's zero-case lemmas.

Import-direction anomaly

This file lives under Combinatorics/ but imports Linglib.Core.Algebra.RootedTree.PreLie.Insertion. The anomaly is temporary: the path-based Insertion.lean is planned to migrate to Combinatorics/RootedTree/Planar/Insertion.lean, after which the imports become hierarchical.

noncomputable def RootedTree.Nonplanar.insertionMultiset {α : Type u_1} (F G : Multiset (Nonplanar α)) : Multiset (Multiset (Nonplanar α))

Multi-tree insertion at the nonplanar level. Given a host forest F and guest forest G (both Multiset (Nonplanar α)), produces the multiset of all forests obtained by inserting G's trees at vertices of F's trees. Defined via list representatives (Multiset.toList) + planar representatives (Quotient.out) + Planar.Pathed.insertionForest.

Equations

• One or more equations did not get rendered due to their size.

theorem RootedTree.Nonplanar.insertionMultiset_zero_right {α : Type u_1} (F : Multiset (Nonplanar α)) : insertionMultiset F 0 = {F}

With no guests, the multi-graft leaves F unchanged: insertionMultiset F 0 = {F}.

theorem RootedTree.Nonplanar.insertionMultiset_zero_left_of_ne_zero {α : Type u_1} (G : Multiset (Nonplanar α)) (h : G ≠ 0) : insertionMultiset 0 G = 0

With no host but non-empty guests, no vertices to graft into: insertionMultiset 0 G = 0.

§2: toList helpers

Multiset's toList returns a non-canonical list representative. Two different choices of representative produce Perm-equivalent lists. Below: a Perm bridge between (M + N).toList and M.toList ++ N.toList, and its Q.out-mapped lift to the planar level. Used by insertionMultiset_add_host to bridge (A + B).toList.map Q.out with the disjoint-host concatenation A.toList.map Q.out ++ B.toList.map Q.out.

theorem Multiset.toList_add_perm {β : Type u_2} (M N : Multiset β) : (M + N).toList.Perm (M.toList ++ N.toList)

(M + N).toList is Perm-equivalent to M.toList ++ N.toList. Both have multiset M + N; Perm follows from Multiset.coe_eq_coe.

[UPSTREAM] candidate: pure Multiset substrate, no rooted-tree dependencies. Belongs in mathlib's Mathlib.Data.Multiset.Basic alongside Multiset.coe_toList and Multiset.coe_add.

theorem RootedTree.Nonplanar.toList_map_quotientOut_add_perm {α : Type u_1} (M N : Multiset (Nonplanar α)) : (List.map Quotient.out (M + N).toList).Perm (List.map Quotient.out M.toList ++ List.map Quotient.out N.toList)

Quotient.out-mapped lift of Multiset.toList_add_perm: at the Planar level, (M + N).toList.map Quotient.out is Perm to M.toList.map Quotient.out ++ N.toList.map Quotient.out.