Nonplanar multi-tree insertion

Lift of RoseTree.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 path-based single/forest insertion operators). The path apparatus currently lives in the Algebra leg; were it to graduate to Combinatorics/, the imports would become strictly 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) + tree representatives (Quotient.out) + RoseTree.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 tree 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 tree level, (M + N).toList.map Quotient.out is Perm to M.toList.map Quotient.out ++ N.toList.map Quotient.out.

theorem RootedTree.Nonplanar.insertionMultiset_card_eq {α : Type u_2} (A B : Multiset (Nonplanar α)) {F' : Multiset (Nonplanar α)} (hF' : F' ∈ insertionMultiset A B) : F'.card = A.card

The insertion multiset preserves cardinality: every forest in insertionMultiset A B has the same cardinality as A.

Proof: insertionMultiset A B is built from insertionForest (A.toList.map Q.out) (B.toList.map Q.out); every output list L has L.length = (A.toList.map Q.out).length = A.card (via RoseTree.Pathed.insertionForest_length); and the cardinality of the lifted Multiset.ofList (L.map mk) equals L.length.

§3: Root-value preservation for singleton hosts

When the host forest is a single tree {T}, every output forest of insertionMultiset {T} B is a singleton {T'} and T'.rootValue = T.rootValue: grafting guests into a tree only modifies its subtrees, never its root value.

The proof descends through the tree substrate using RoseTree.Pathed.insertionForest_singleton and multiGraft_node (which preserves the head value by structure).

theorem RootedTree.Nonplanar.insertionMultiset_singleton_rootValue {α : Type u_1} (T : Nonplanar α) (B : Multiset (Nonplanar α)) {F' : Multiset (Nonplanar α)} (hF' : F' ∈ insertionMultiset {T} B) : ∃ (T' : Nonplanar α), F' = {T'} ∧ T'.rootValue = T.rootValue

Singleton-host root preservation: every forest in insertionMultiset {T} B is a singleton {T'} and T'.rootValue = T.rootValue. Descends through insertionForest_singleton + RoseTree.value_multiGraft.