Singleton-guest composition of the multi-graft insertion

Inserting one further guest v into the outputs of a simultaneous multi-graft decomposes as: v lands at an original host vertex (extending the simultaneous graft), or inside one of the grafted guest copies (pre-grafting that guest). This is the single-guest case of the multi-graft associativity (Oudom-Guin Prop 2.7.v at the basis level) and the combinatorial content of the Grossman-Larson guest-splitting identity GL_product_split_mul_ι.

Main results

• insertion_multiGraft_singleton: per grafted output, the two-class decomposition of single-guest insertion, via multiGraft_cons_pair (original vertices) and multiGraft_split_lifted_aux (guest copies).
• insertion_bind_singleton: tree-host form, (insertion T B).bind (insertion · [v]) = insertion T (v :: B) + (insertionForest B [v]).bind (insertion T ·).
• insertionForest_bind_singleton: forest-host form of the same.

All statements are validated computationally on concrete trees, including the raw (RoseTree-level multiset, not quotient-level) forms of the last two.

Two-class form of the grafted-vertex decomposition

theorem RoseTree.Pathed.vertices_multiGraft_transport_lift {α : Type u_1} (T : RoseTree α) (pairs : List (Path × RoseTree α)) (h_valid : ∀ (pair : Path × RoseTree α), pair ∈ pairs → IsValidPath pair.1 T) : ↑(vertices (multiGraft T pairs)) = Multiset.map (transport pairs) ↑(vertices T) + (↑(List.finRange pairs.length)).bind fun (k : Fin pairs.length) => Multiset.map (liftMulti pairs k) ↑(vertices pairs[k].2)

The vertex multiset of a grafted tree: transported originals plus lifted guest vertices. Collapses the three classes of vertices_multiGraft_decomp (preserveMulti is transport off pairSources).

Single-guest insertion as a vertex sum

theorem RoseTree.Pathed.insertion_singleton_guest {α : Type u_1} (W v : RoseTree α) : insertion W [v] = Multiset.map (fun (p : Path) => insertAt p v W) ↑(vertices W)

Single-guest insertion grafts the guest at each host vertex.

Per-output decomposition

theorem RoseTree.Pathed.insertion_multiGraft_singleton {α : Type u_1} (T : RoseTree α) (pairs : List (Path × RoseTree α)) (v : RoseTree α) (h_valid : ∀ (pair : Path × RoseTree α), pair ∈ pairs → IsValidPath pair.1 T) : insertion (multiGraft T pairs) [v] = Multiset.map (fun (u : Path) => multiGraft T ((u, v) :: pairs)) ↑(vertices T) + (↑(List.finRange pairs.length)).bind fun (k : Fin pairs.length) => Multiset.map (fun (q : Path) => multiGraft T (pairs.set ↑k (pairs[k].1, insertAt q v pairs[k].2))) ↑(vertices pairs[k].2)

Inserting one guest v into a multi-graft output: v lands at an original vertex (prepend the pair) or inside the k-th grafted guest (pre-graft that guest).

Singleton-guest associativity

theorem RoseTree.Pathed.insertionForest_singleton_guest_set {α : Type u_1} (B : List (RoseTree α)) (v : RoseTree α) : insertionForest B [v] = (↑(List.finRange B.length)).bind fun (k : Fin B.length) => Multiset.map (fun (q : Path) => B.set (↑k) (insertAt q v B[k])) ↑(vertices B[k])

Decomposition of insertionForest B [v]: insert v into each position of each tree of B. De-privatized 2026-06-12 for GL_T2_reindexing_key (Q5c) which needs length-preservation of single-guest insertion outputs.

theorem RoseTree.Pathed.insertion_bind_singleton {α : Type u_1} (T : RoseTree α) (B : List (RoseTree α)) (v : RoseTree α) : ((insertion T B).bind fun (W : RoseTree α) => insertion W [v]) = insertion T (v :: B) + (insertionForest B [v]).bind fun (B' : List (RoseTree α)) => insertion T B'

RoseTree-host singleton-guest associativity: grafting B then one more guest v equals grafting v :: B simultaneously plus grafting B with v nested into one of its trees. Raw RoseTree-level multiset equality.

theorem RoseTree.Pathed.insertionForest_singleton_bucket_split {α : Type u_1} {γ : Type u_2} (B : List (RoseTree α)) (m : List Bool) (v : RoseTree α) (G : List (RoseTree α) → List (RoseTree α) → Multiset γ) (hlen : m.length = B.length) : ((insertionForest B [v]).bind fun (B' : List (RoseTree α)) => G (List.filterMap (fun (p : RoseTree α × Bool) => if p.2 = true then some p.1 else none) (B'.zip m)) (List.filterMap (fun (p : RoseTree α × Bool) => if p.2 = true then none else some p.1) (B'.zip m))) = ((insertionForest (List.filterMap (fun (p : RoseTree α × Bool) => if p.2 = true then some p.1 else none) (B.zip m)) [v]).bind fun (W : List (RoseTree α)) => G W (List.filterMap (fun (p : RoseTree α × Bool) => if p.2 = true then none else some p.1) (B.zip m))) + (insertionForest (List.filterMap (fun (p : RoseTree α × Bool) => if p.2 = true then none else some p.1) (B.zip m)) [v]).bind fun (W' : List (RoseTree α)) => G (List.filterMap (fun (p : RoseTree α × Bool) => if p.2 = true then some p.1 else none) (B.zip m)) W'

Bucketing lemma: single-guest insertion insertionForest B [v] modifies exactly one position of B, so after partitioning each output B' into a t-bucket and f-bucket according to a fixed mask m (of length B.length), the modification appears in exactly one of the two buckets. The factored form, summing over a general consumer G, lets us instantiate G to the cons-assignment body in insertionForest_bind_singleton.

De-privatized 2026-06-12 for GL_product_split_mul_ι (Q5c per-tprod induction): the same bucket-split, after descent through the listChoices_bridge_powerset_paired translation, supplies the reindexing for T2 = F * insertion (op G) (op of'{v}) against the powerset-of-B sum produced by mul_of'_sum_form + Leibniz on the other terms.

theorem RoseTree.Pathed.insertionForest_bind_singleton {α : Type u_1} (A B : List (RoseTree α)) (v : RoseTree α) : ((insertionForest A B).bind fun (X : List (RoseTree α)) => insertionForest X [v]) = insertionForest A (v :: B) + (insertionForest B [v]).bind fun (B' : List (RoseTree α)) => insertionForest A B'

Forest-host singleton-guest associativity. Raw RoseTree-level multiset equality; the nonplanar insertionMultiset form follows by the standard quotient descent.