Foissy 2021 Theorem 5.1 multi-tree insertion (path-based)

@cite{foissy-typed-decorated-rooted-trees-2018} @cite{foissy-introduction-hopf-algebras-trees}

The Foissy 2021 Theorem 5.1 multi-tree multi-vertex insertion operator. Defined as a sum over functions Ts → V(T) of multiGraft, taken as a Multiset to make the sum-over-choices commutative.

Sibling to Graft.lean (path-based multi-graft primitive). Lives under namespace RootedTree.Planar.Pathed for now; the Pathed sub-namespace will be hoisted to RootedTree.Planar once the legacy Vertex.lean consumers (InsertSum.lean, Algebra.lean, VertexBijection.lean) migrate to the path-based representation.

File scope

• §1: listChoices — choice-list enumeration (representation-independent).
• §2: insertion — Foissy 2021 Theorem 5.1, single-tree host.
• §3: insertionForest — forest host (Foissy 2021 §5.1) + identity/nil lemmas.
• §4: Pair-list Perm-invariance (multiGraft_perm_pair).
• §5: Guest-list invariance (insertion_perm_guests, insertion_planarEquiv_guests).
• §6: Host invariance substrate — swapPathAt path-relabel bijection, vertices_swap_perm, multiGraft_swap_planarEquiv, insertion_planarEquiv_host.
• §7: Forest invariance variants.

Status

[UPSTREAM] candidate. Sorry-free.

• §1–§5: sorry-free.
• §6 (multiGraft_swap_planarEquiv, insertion_planarEquiv_host): sorry-free. Architecture: PlanarStep.exists_pathBijection gives, for any PlanarStep t t', a path bijection f satisfying both ((vertices t).map f).Perm (vertices t') and the multiGraft-equivalent after pair relabel. Built by induction on the step (swap uses swapPathAt n; recurse uses pathLiftRecurse n of inner bijection). insertion_eq_of_pathBij is the generic lifter from path bijection to mk-equality of insertions. Together they yield insertion_planarStep_host in two lines; the outer EqvGen induction finishes insertion_planarEquiv_host.
• §7 (insertionForest_planarEquiv_host): sorry-free. Induction on Forall₂ PlanarEquiv; cons case lifts via Multiset.map_bind + Multiset.bind_map + insertion_planarEquiv_host (head) + IH (tail).
• §7 (insertionForest_perm_guests): sorry-free. Outer induction on F; cons-F case routes through forestPairSum, a Multiset aggregator that splits the guest list into pre_T (going to the head host) and pre_F (going to the tail forest). The bridge forestPairSum_eq_insertionForest reduces to the canonical insertionForest; Perm invariance is then established via forestPairSum_pre_perm_mk (Perm of accumulators, using insertion_perm_guests for the head + the outer F-IH for the tail) + forestPairSum_swap_mk (adjacent swap via Multiset.bind_bind + the pre-perm lemma) + induction on List.Perm.

§1: listChoices enumeration

def RootedTree.Planar.Pathed.listChoices {β : Type u_2} : List β → ℕ → List (List β)

All length-n lists with entries from xs (with repetition). The "n-fold list power" used in Foissy 2021 Theorem 5.1's vertex-choice sum. Representation-independent (no Vertex dependence): copied from the legacy Insertion.lean.

Equations

• RootedTree.Planar.Pathed.listChoices x✝ 0 = [[]]
• RootedTree.Planar.Pathed.listChoices x✝ n.succ = List.flatMap (fun (v : β) => List.map (fun (x : List β) => v :: x) (RootedTree.Planar.Pathed.listChoices x✝ n)) x✝

@[simp]

theorem RootedTree.Planar.Pathed.listChoices_zero {β : Type u_2} (xs : List β) : listChoices xs 0 = [[]]

@[simp]

theorem RootedTree.Planar.Pathed.listChoices_succ {β : Type u_2} (xs : List β) (n : ℕ) : listChoices xs (n + 1) = List.flatMap (fun (v : β) => List.map (fun (x : List β) => v :: x) (listChoices xs n)) xs

§2: insertion — Foissy 2021 Theorem 5.1

def RootedTree.Planar.Pathed.insertion {α : Type u_1} (T : Planar α) (Ts : List (Planar α)) : Multiset (Planar α)

Foissy 2021 Theorem 5.1 multi-graft on a single-tree host. Sum over (v₁, …, vₙ) ∈ V(T)ⁿ of multiGraft T [(v₁, T₁), …, (vₙ, Tₙ)].

Equations

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

theorem RootedTree.Planar.Pathed.insertion_def {α : Type u_1} (T : Planar α) (Ts : List (Planar α)) : insertion T Ts = ↑(List.map (fun (choice : List Path) => multiGraft T (choice.zip Ts)) (listChoices (vertices T) Ts.length))

§3: insertionForest — forest host

@[irreducible]

def RootedTree.Planar.Pathed.insertionForest {α : Type u_1} : List (Planar α) → List (Planar α) → Multiset (List (Planar α))

Multi-graft into a host forest. Disjoint pattern cases for clean auto-generated equation lemmas.

Equations

• One or more equations did not get rendered due to their size.
• RootedTree.Planar.Pathed.insertionForest [] [] = {[]}
• RootedTree.Planar.Pathed.insertionForest [] (head :: tail) = 0
• RootedTree.Planar.Pathed.insertionForest (T :: F) [] = {T :: F}

@[simp]

theorem RootedTree.Planar.Pathed.insertionForest_nil_nil {α : Type u_1} : insertionForest [] [] = {[]}

@[simp]

theorem RootedTree.Planar.Pathed.insertionForest_empty_host_nonempty_guests {α : Type u_1} (T_g : Planar α) (Ts : List (Planar α)) : insertionForest [] (T_g :: Ts) = 0

@[simp]

theorem RootedTree.Planar.Pathed.insertionForest_cons_host_nil_guests {α : Type u_1} (T : Planar α) (F : List (Planar α)) : insertionForest (T :: F) [] = {T :: F}

theorem RootedTree.Planar.Pathed.insertionForest_nil_guests {α : Type u_1} (F : List (Planar α)) : insertionForest F [] = {F}

theorem RootedTree.Planar.Pathed.insertionForest_cons_cons {α : Type u_1} (T : Planar α) (F : List (Planar α)) (T_g : Planar α) (Ts : List (Planar α)) : insertionForest (T :: F) (T_g :: Ts) = (↑(listChoices [true, false] (T_g :: Ts).length)).bind fun (assignment : List Bool) => (insertion T (List.filterMap (fun (p : Planar α × Bool) => if p.2 = true then some p.1 else none) ((T_g :: Ts).zip assignment))).bind fun (T' : Planar α) => Multiset.map (fun (F' : List (Planar α)) => T' :: F') (insertionForest F (List.filterMap (fun (p : Planar α × Bool) => if p.2 = true then none else some p.1) ((T_g :: Ts).zip assignment)))

§4: Pair-list Perm invariance for multiGraft

multiGraft T pairs is PlanarEquiv-invariant under permutation of the pair list: grafts at distinct paths commute, and grafts at the same path are root-list permutations (lift via planarEquiv_root_perm).

Path-based reformulation of the legacy multiGraft_perm_pair / multiGraftList_perm_pair.

theorem RootedTree.Planar.Pathed.multiGraft_perm_pair {α : Type u_1} (T : Planar α) {pairs pairs' : List (Path × Planar α)} : pairs.Perm pairs' → (multiGraft T pairs).PlanarEquiv (multiGraft T pairs')

PlanarEquiv of multiGraft T pairs and multiGraft T pairs' follows from a List.Perm between pairs and pairs'. Mutual recursion on T with the children-list aux.

theorem RootedTree.Planar.Pathed.multiGraftChildren_perm_pair {α : Type u_1} (cs : List (Planar α)) {pairs pairs' : List (Path × Planar α)} : pairs.Perm pairs' → List.Forall₂ PlanarEquiv (multiGraftChildren cs pairs) (multiGraftChildren cs pairs')

List-level companion to multiGraft_perm_pair: pair-list Perm lifts to Forall₂ PlanarEquiv on the children list output of multiGraftChildren.

Forall₂-version of multiGraft_perm_pair

For insertion_planarEquiv_guests we need: when Ts ~ᶠ Ts' (Forall₂ PlanarEquiv) and we zip with the same choice, the resulting pair lists satisfy a Forall₂ relation (same fst, PlanarEquiv snd). Then this lifts to multiGraft T pairs ~ multiGraft T pairs' (PlanarEquiv).

Path-based version of the legacy multiGraft_planarEquiv_pair_Forall₂.

§5: Guest-list invariance for insertion

pairSum t pre Ts aggregates mk (multiGraft t (pre ++ c.zip Ts)) over all choices c ∈ listChoices (vertices t) |Ts|. The clean recursive equation pairSum t pre (x :: rest) = bind v over vertices of pairSum t (pre ++ [(v, x)]) rest lets us prove Ts-perm invariance by Perm induction.

Path-based reformulation of the legacy pairSum / insertion_perm_guests machinery. The pair type changes from Vertex t × Planar α to Path × Planar α.

theorem RootedTree.Planar.Pathed.insertion_perm_guests {α : Type u_1} (t : Planar α) {Ts Ts' : List (Planar α)} (h : Ts.Perm Ts') : Multiset.map Nonplanar.mk (insertion t Ts) = Multiset.map Nonplanar.mk (insertion t Ts')

Single-tree insertion is mk-invariant under List.Perm of guests.

theorem RootedTree.Planar.Pathed.insertion_planarEquiv_guests {α : Type u_1} (t : Planar α) {Ts Ts' : List (Planar α)} (h : List.Forall₂ PlanarEquiv Ts Ts') : Multiset.map Nonplanar.mk (insertion t Ts) = Multiset.map Nonplanar.mk (insertion t Ts')

Guest-list Forall₂ PlanarEquiv lifts to insertion mk-equality.

§5.5: Validity discharge for multiGraft_compose at canonical shapes

When the outer-pair list has the canonical shape choice.zip Ts with choice ∈ listChoices (vertices T) Ts.length, the validity hypothesis of multiGraft_compose (every pair's .fst is a valid path in the host) discharges automatically via forall_isValidPath lifted from mem_of_mem_listChoices.

Why this lives here and not in Graft.lean: listChoices is defined in Insertion.lean §1, but multiGraft_compose is defined in Graft.lean §11. The validity bridge crossing between them belongs here.

Consumer status (2026-05-16): previously used by the A3.3 basis-level helpers (deleted with InsertionAssoc.lean). These specializations remain as general-purpose validity-discharge utilities for any caller working with listChoices-derived pair lists.

theorem RootedTree.Planar.Pathed.mem_of_mem_listChoices {β : Type u_2} (xs : List β) (n : ℕ) (choice : List β) (h_choice : choice ∈ listChoices xs n) (v : β) (h_v : v ∈ choice) : v ∈ xs

Every element of a choice ∈ listChoices xs n is a member of xs. Lifts membership-in-an-enumerated-choice to membership-in-the-alphabet.

theorem RootedTree.Planar.Pathed.forall_zip_isValidPath_of_listChoices {α : Type u_1} (T : Planar α) (Ts : List (Planar α)) (choice : List Path) (h_choice : choice ∈ listChoices (vertices T) Ts.length) (pair : Path × Planar α) (h_pair : pair ∈ choice.zip Ts) : IsValidPath pair.1 T

Every path in a choice.zip Ts pair list is a valid path in T, when choice ∈ listChoices (vertices T) Ts.length. Discharges the h_outer_valid hypothesis of multiGraft_compose for the canonical A3.3 outer pair shape.

theorem RootedTree.Planar.Pathed.multiGraft_compose_at_choice {α : Type u_1} (T : Planar α) (outer_Ts : List (Planar α)) (choice_o : List Path) (h_choice_o : choice_o ∈ listChoices (vertices T) outer_Ts.length) (inner_pairs : List (Path × Planar α)) (h_inner_valid : ∀ (p : Path × Planar α), p ∈ inner_pairs → IsValidPath p.1 (multiGraft T (choice_o.zip outer_Ts))) : multiGraft (multiGraft T (choice_o.zip outer_Ts)) inner_pairs = multiGraft T (composePairs (choice_o.zip outer_Ts) inner_pairs)

Auto-discharge variant of multiGraft_compose for the canonical A3.3 outer-pair shape choice_o.zip outer_Ts with choice_o ∈ listChoices (vertices T) outer_Ts.length. The inner pair list's validity is passed as a hypothesis.

theorem RootedTree.Planar.Pathed.multiGraft_compose_at_choice_inner_zip {α : Type u_1} (T : Planar α) (outer_Ts : List (Planar α)) (choice_o : List Path) (h_choice_o : choice_o ∈ listChoices (vertices T) outer_Ts.length) (inner_Ts : List (Planar α)) (choice_i : List Path) (h_choice_i : choice_i ∈ listChoices (vertices (multiGraft T (choice_o.zip outer_Ts))) inner_Ts.length) : multiGraft (multiGraft T (choice_o.zip outer_Ts)) (choice_i.zip inner_Ts) = multiGraft T (composePairs (choice_o.zip outer_Ts) (choice_i.zip inner_Ts))

Doubly auto-discharged variant: both outer and inner choices come from listChoices-derived enumerations. Specifically for the A3.3 TRUE-side shape where inner = (v_c :: ch).zip (c :: filter_t) with v_c ∈ vertices T' and ch ∈ listChoices (vertices T') filter_t.length.

theorem RootedTree.Planar.Pathed.multiGraft_compose_cons_pair_at_choice {α : Type u_1} (T : Planar α) (outer_Ts : List (Planar α)) (choice_o : List Path) (h_choice_o : choice_o ∈ listChoices (vertices T) outer_Ts.length) (filter_t : List (Planar α)) (c : Planar α) (v_c : Path) (h_v_c : v_c ∈ vertices (multiGraft T (choice_o.zip outer_Ts))) (ch : List Path) (h_ch : ch ∈ listChoices (vertices (multiGraft T (choice_o.zip outer_Ts))) filter_t.length) : multiGraft (multiGraft T (choice_o.zip outer_Ts)) ((v_c, c) :: ch.zip filter_t) = multiGraft T (composePairs (choice_o.zip outer_Ts) ((v_c, c) :: ch.zip filter_t))

Cons-form specialization for the A3.3 TRUE-side pattern: the inner pair list has shape (v_c, c) :: ch.zip filter_t where v_c ∈ vertices T' and ch ∈ listChoices (vertices T') filter_t.length. The output of multiGraft_compose_at_choice becomes a single multiGraft T with composePairs building the combined pair list.

theorem RootedTree.Planar.Pathed.vc_partition_via_bind {α : Type u_1} {γ : Type u_2} (T : Planar α) (pairs : List (Path × Planar α)) (h_valid : ∀ (pair : Path × Planar α), pair ∈ pairs → IsValidPath pair.1 T) (f : Path → Multiset γ) : (↑(vertices (multiGraft T pairs))).bind f = (Multiset.filterMap (preserveMulti pairs) ↑(vertices T)).bind f + (Multiset.map (transport pairs) (Multiset.filter (fun (x : Path) => x ∈ pairSources pairs) ↑(vertices T))).bind f + ((↑(List.finRange pairs.length)).bind fun (k : Fin pairs.length) => Multiset.map (liftMulti pairs k) ↑(vertices pairs[k].2)).bind f

Distribute vertices_multiGraft_decomp's 3-class partition through a bind over Multiset.ofList (vertices (multiGraft T pairs)). The v_c bind in the A3.3 TRUE-side helper has exactly this shape; after this rewrite, the bind splits into 3 binds (one per class), each ready for per-class absorption (Sessions 2-3 substrate).

theorem RootedTree.Planar.Pathed.vc_partition_forest_via_bind {α : Type u_1} {γ : Type u_2} (cs : List (Planar α)) (per_tree_pairs : Fin cs.length → List (Path × Planar α)) (h_valid : ∀ (i : Fin cs.length) (pair : Path × Planar α), pair ∈ per_tree_pairs i → IsValidPath pair.1 cs[↑i]) (offset : ℕ) (f : Path → Multiset γ) : (↑(verticesAux offset (List.map (fun (i : Fin cs.length) => multiGraft cs[↑i] (per_tree_pairs i)) (List.finRange cs.length)))).bind f = (↑(List.finRange cs.length)).bind fun (i : Fin cs.length) => (Multiset.map (fun (x : List ℕ) => (offset + ↑i) :: x) (Multiset.filterMap (preserveMulti (per_tree_pairs i)) ↑(vertices cs[↑i]) + Multiset.map (transport (per_tree_pairs i)) (Multiset.filter (fun (x : Path) => x ∈ pairSources (per_tree_pairs i)) ↑(vertices cs[↑i])) + (↑(List.finRange (per_tree_pairs i).length)).bind fun (k : Fin (per_tree_pairs i).length) => Multiset.map (liftMulti (per_tree_pairs i) k) ↑(vertices (per_tree_pairs i)[↑k].2))).bind f

F-side analog: distribute vertices_forest_eq_partition's per-tree 3-class partition through a bind over Multiset.ofList (verticesAux 0 (forest as constructed)). Specifically the A3.3 FALSE-side helper binds over the F'-side vertex enumeration, which has this shape with cs = F_A (preserved + sourceSelf) and per-tree lifted into pre_FA_B.

NOTE: the FALSE side of A3.3 actually binds over perKFChoice F' not raw vertices of F'; see perKFChoice_eq_forest_bind (Session 4 substrate) for the bridge from perKFChoice enumeration to vertex enumeration with per-tree (i, v) pairs. This lemma is the raw vertex form; pair with the forthcoming bridge to get the perKFChoice form.

theorem RootedTree.Planar.Pathed.insertion_cons_pair_eq_bind {α : Type u_1} (T c : Planar α) (filter_t : List (Planar α)) : insertion T (c :: filter_t) = (↑(vertices T)).bind fun (v_c : Path) => ↑(List.map (fun (ch : List Path) => multiGraft T ((v_c, c) :: ch.zip filter_t)) (listChoices (vertices T) filter_t.length))

Decompose insertion T (c :: filter_t) by extracting the leading vertex v_c as a bind variable. The first vertex choice routes c; the remaining filter_t.length choices route the rest of the guests.

theorem RootedTree.Planar.Pathed.insertion_cons_pair_at_multiGraft_bind {α : Type u_1} {γ : Type u_2} (T : Planar α) (pairs : List (Path × Planar α)) (h_valid : ∀ (pair : Path × Planar α), pair ∈ pairs → IsValidPath pair.1 T) (c : Planar α) (filter_t : List (Planar α)) (K : Planar α → Multiset γ) : (insertion (multiGraft T pairs) (c :: filter_t)).bind K = ((Multiset.map (transport pairs) ↑(vertices T)).bind fun (v_c : Path) => (↑(List.map (fun (ch : List Path) => multiGraft (multiGraft T pairs) ((v_c, c) :: ch.zip filter_t)) (listChoices (vertices (multiGraft T pairs)) filter_t.length))).bind K) + ((↑(List.finRange pairs.length)).bind fun (k : Fin pairs.length) => Multiset.map (liftMulti pairs k) ↑(vertices pairs[k].2)).bind fun (v_c : Path) => (↑(List.map (fun (ch : List Path) => multiGraft (multiGraft T pairs) ((v_c, c) :: ch.zip filter_t)) (listChoices (vertices (multiGraft T pairs)) filter_t.length))).bind K

Combined form for insertion (multiGraft T pairs) (c :: filter_t) binding into a function K: the v_c bind splits into preserved + sourceSelf + lifted via vc_partition_via_bind, with each class producing a sub-bind over ch ∈ listChoices (vertices (multiGraft T pairs)) filter_t.length.

§5.6: A3.3 substrate — Session 3 auto-discharge specializations

Specializations of insertion_cons_pair_at_multiGraft_bind for the canonical A3.3 outer-pair shape pairs = choice.zip Ts with choice ∈ listChoices (vertices T) Ts.length. The validity hypothesis is auto-discharged via forall_zip_isValidPath_of_listChoices.

Used by LHS_TRUE_eq_T_buckets (and Session 4's analog) to split the inner (insertion T' (c :: filter_t)).bind K into preserved+sourceSelf and lifted classes WITHOUT requiring the proof to discharge validity inline.

theorem RootedTree.Planar.Pathed.insertion_cons_pair_at_multiGraft_bind_at_choice {α : Type u_1} {γ : Type u_2} (T : Planar α) (Ts : List (Planar α)) (choice : List Path) (h_choice : choice ∈ listChoices (vertices T) Ts.length) (c : Planar α) (filter_t : List (Planar α)) (K : Planar α → Multiset γ) : (insertion (multiGraft T (choice.zip Ts)) (c :: filter_t)).bind K = ((Multiset.map (transport (choice.zip Ts)) ↑(vertices T)).bind fun (v_c : Path) => (↑(List.map (fun (ch : List Path) => multiGraft (multiGraft T (choice.zip Ts)) ((v_c, c) :: ch.zip filter_t)) (listChoices (vertices (multiGraft T (choice.zip Ts))) filter_t.length))).bind K) + ((↑(List.finRange (choice.zip Ts).length)).bind fun (k : Fin (choice.zip Ts).length) => Multiset.map (liftMulti (choice.zip Ts) k) ↑(vertices (choice.zip Ts)[k].2)).bind fun (v_c : Path) => (↑(List.map (fun (ch : List Path) => multiGraft (multiGraft T (choice.zip Ts)) ((v_c, c) :: ch.zip filter_t)) (listChoices (vertices (multiGraft T (choice.zip Ts))) filter_t.length))).bind K

Auto-discharge specialization of insertion_cons_pair_at_multiGraft_bind for the canonical A3.3 shape pairs = choice.zip Ts. The validity hypothesis is supplied internally via forall_zip_isValidPath_of_listChoices.

theorem RootedTree.Planar.Pathed.insertion_outer_bind_at_choice_eq {α : Type u_1} {γ : Type u_2} (T : Planar α) (Ts : List (Planar α)) (K : Planar α → Multiset γ) : (insertion T Ts).bind K = (↑(listChoices (vertices T) Ts.length)).bind fun (choice : List Path) => K (multiGraft T (choice.zip Ts))

Unfold (insertion T Ts).bind K to its choice-bind form, exposing the choice ∈ listChoices (vertices T) Ts.length bind variable so that mG T (choice.zip Ts) is substituted into K. Bridge from the abstract insertion T Ts form to the concrete pair-list-choice form needed for insertion_cons_pair_at_multiGraft_bind_at_choice.

Proof: unfold insertion_def, then ← Multiset.map_coe + Multiset.bind_map to expose choice as the bind variable.

theorem RootedTree.Planar.Pathed.listChoices_bind_insertion_inner_split {α : Type u_1} {γ : Type u_2} (T : Planar α) (Ts : List (Planar α)) (c : Planar α) (filter_t : List (Planar α)) (K : List Path → Planar α → Multiset γ) : ((↑(listChoices (vertices T) Ts.length)).bind fun (choice : List Path) => (insertion (multiGraft T (choice.zip Ts)) (c :: filter_t)).bind (K choice)) = ((↑(listChoices (vertices T) Ts.length)).bind fun (choice : List Path) => (Multiset.map (transport (choice.zip Ts)) ↑(vertices T)).bind fun (v_c : Path) => (↑(List.map (fun (ch : List Path) => multiGraft (multiGraft T (choice.zip Ts)) ((v_c, c) :: ch.zip filter_t)) (listChoices (vertices (multiGraft T (choice.zip Ts))) filter_t.length))).bind (K choice)) + (↑(listChoices (vertices T) Ts.length)).bind fun (choice : List Path) => ((↑(List.finRange (choice.zip Ts).length)).bind fun (k : Fin (choice.zip Ts).length) => Multiset.map (liftMulti (choice.zip Ts) k) ↑(vertices (choice.zip Ts)[k].2)).bind fun (v_c : Path) => (↑(List.map (fun (ch : List Path) => multiGraft (multiGraft T (choice.zip Ts)) ((v_c, c) :: ch.zip filter_t)) (listChoices (vertices (multiGraft T (choice.zip Ts))) filter_t.length))).bind (K choice)

Bundled substrate for Session 4: the bind-over-listChoices composed with the inner cons-pair split. Discharges h_choice internally via Multiset.mem_coe. The K parameter is universally quantified over the choice (so it can carry context from outer binds in the calling proof).

Use this when the goal has form (Mset.ofList (lC vT Ts.length)).bind (fun choice => (insertion (mG T (choice.zip Ts)) (c :: filter_t)).bind (K choice)) and you want to split the inner bind into preserved+lifted classes without manually peeling the choice-bind via Multiset.bind_congr.

§5.7: composePairs_planarEquiv_partition — partition of composePairs result

The PE-level partition theorem for composePairs (defined in Graft.lean §11). For an outer pair list and inner pair list (with inner paths valid in mG T outer), applying multiGraft T to composePairs outer inner is PE-equivalent (at Nonplanar.mk level) to applying multiGraft T to:

• For each k : Fin outer.length: outer[k] modified to have its .snd multi-grafted with liftedInnerAt outer inner k (the inner pairs lifted into outer[k]'s subtree, with paths stripped via stripLiftMulti).
• Plus rootInner outer inner: the preserved/sourceSelf inner pairs with paths untransported back to T-coordinates via untransport.

DEPRECATED 2026-05-16 as critical-path substrate. Off the GL associativity path under the abstract OG pivot (scratch/pivot_to_prelie_pbw.md, Linglib/Core/Algebra/PreLie/OudomGuinCirc.lean). Sorry remains; the helpers liftedInnerAt/rootInner are kept as generic vertex-decomposition primitives.

theorem RootedTree.Planar.Pathed.composePairs_planarEquiv_partition {α : Type u_1} (T : Planar α) (outer inner : List (Path × Planar α)) (_h_outer_valid : ∀ (p : Path × Planar α), p ∈ outer → IsValidPath p.1 T) (_h_inner_valid : ∀ (p : Path × Planar α), p ∈ inner → IsValidPath p.1 (multiGraft T outer)) : Nonplanar.mk (multiGraft T (composePairs outer inner)) = Nonplanar.mk (multiGraft T (List.map (fun (k : Fin outer.length) => (outer[↑k].1, multiGraft outer[↑k].2 (liftedInnerAt outer inner k))) (List.finRange outer.length) ++ rootInner outer inner))

Partition assembly: applying multiGraft T to composePairs outer inner is PE-equivalent (at Nonplanar level) to applying multiGraft T to the assembled per-outer-k sub-multiGrafts plus untransported root inner.

§6: Host invariance via path-swap bijection

insertion T Ts is mk-invariant under PlanarEquiv of the host: the original blocker for the path-based refactor.

Strategy:

1. swapPathAt n — swap the first index n ↔ n+1 in a path.
2. vertices_swap_perm — applying swapPathAt pre.length to vertices of node a (pre ++ l :: r :: post) is a List.Perm of vertices of node a (pre ++ r :: l :: post). Reduces to a List.Perm of two appendable middle blocks, via verticesAux_append + a List.perm_append_comm.
3. multiGraft_swap_planarEquiv — the multiGraft results differ only by the swap of l/r in the root children list; lift via PlanarStep.swapAtRoot.
4. Combine via listChoices Perm-respect → insertion_swap_invariant.
5. Lift via PlanarStep (recurse case) and PlanarEquiv = EqvGen PlanarStep.

def RootedTree.Planar.Pathed.swapPathAt (n : ℕ) : Path → Path

Swap the first index n ↔ n+1 of a path. Acts as identity on paths starting outside {n, n+1} and on the root path [].

Equations

• RootedTree.Planar.Pathed.swapPathAt n [] = []
• RootedTree.Planar.Pathed.swapPathAt n (i :: rest) = if i = n then (n + 1) :: rest else if i = n + 1 then n :: rest else i :: rest

@[simp]

theorem RootedTree.Planar.Pathed.swapPathAt_nil (n : ℕ) : swapPathAt n [] = []

theorem RootedTree.Planar.Pathed.swapPathAt_cons_eq (n : ℕ) (rest : Path) : swapPathAt n (n :: rest) = (n + 1) :: rest

theorem RootedTree.Planar.Pathed.swapPathAt_cons_eq_succ (n : ℕ) (rest : Path) : swapPathAt n ((n + 1) :: rest) = n :: rest

theorem RootedTree.Planar.Pathed.swapPathAt_cons_of_ne (n i : ℕ) (rest : Path) (h1 : i ≠ n) (h2 : i ≠ n + 1) : swapPathAt n (i :: rest) = i :: rest

@[simp]

theorem RootedTree.Planar.Pathed.swapPathAt_involution (n : ℕ) (p : Path) : swapPathAt n (swapPathAt n p) = p

theorem RootedTree.Planar.Pathed.vertices_swap_perm {α : Type u_1} (a : α) (pre : List (Planar α)) (l r : Planar α) (post : List (Planar α)) : (List.map (swapPathAt pre.length) (vertices (node a (pre ++ l :: r :: post)))).Perm (vertices (node a (pre ++ r :: l :: post)))

Vertices of node a (pre ++ l :: r :: post) mapped through swapPathAt pre.length is a List.Perm of vertices of node a (pre ++ r :: l :: post).

§6.2 substrate: pair-relabel + planarEquiv prefix-cons-lift

theorem RootedTree.Planar.Pathed.multiGraft_swap_planarEquiv {α : Type u_1} (a : α) (pre : List (Planar α)) (l r : Planar α) (post : List (Planar α)) (pairs : List (Path × Planar α)) : (multiGraft (node a (pre ++ l :: r :: post)) pairs).PlanarEquiv (multiGraft (node a (pre ++ r :: l :: post)) (List.map (RootedTree.Planar.Pathed.pathRelabelSwap✝ pre.length) pairs))

multiGraft is PlanarEquiv-invariant under swap of two adjacent root children, with pairs relabeled via swapPathAt. The proof decomposes both sides into matching children lists (up to a single swap), then applies PlanarStep.swapAtRoot.

Sub-lemmas for the filter equalities are proved inline as have statements to ensure the inline-match expressions unify with the matcher generated by multiGraft_node.

§6.3 substrate for insertion_planarEquiv_host

The swapAtRoot case of insertion_planarStep_host needs to lift a Perm of vertices into a Perm of choice lists (via listChoices), then combine with multiGraft_swap_planarEquiv to get equal mk-mapped insertion outputs. Helpers below build this bridge.

theorem RootedTree.Planar.Pathed.listChoices_map {β : Type u_2} {γ : Type u_3} (f : β → γ) (xs : List β) (n : ℕ) : listChoices (List.map f xs) n = List.map (List.map f) (listChoices xs n)

listChoices is compatible with List.map: applying f element-wise to choices in xs.map f gives the same as mapping List.map f over listChoices xs n.

theorem RootedTree.Planar.Pathed.listChoices_perm {β : Type u_2} {xs ys : List β} (h : xs.Perm ys) (n : ℕ) : (listChoices xs n).Perm (listChoices ys n)

listChoices respects List.Perm of the source: a Perm of xs and ys lifts to a Perm of listChoices xs n and listChoices ys n.

theorem RootedTree.Planar.Pathed.insertion_planarEquiv_host {α : Type u_1} (Ts : List (Planar α)) {t t' : Planar α} (h : t.PlanarEquiv t') : Multiset.map Nonplanar.mk (insertion t Ts) = Multiset.map Nonplanar.mk (insertion t' Ts)

insertion T Ts is mk-invariant under PlanarEquiv of the host.

theorem RootedTree.Planar.Pathed.insertionForest_planarEquiv_host {α : Type u_1} (Ts : List (Planar α)) {F F' : List (Planar α)} (h : List.Forall₂ PlanarEquiv F F') : Multiset.map (List.map Nonplanar.mk) (insertionForest F Ts) = Multiset.map (List.map Nonplanar.mk) (insertionForest F' Ts)

Forest host invariance: Forall₂ PlanarEquiv F F' lifts to mk-equality of insertionForest F Ts and insertionForest F' Ts.

§7.1 substrate for insertionForest_perm_guests

Forest-side analogue of pairSum: a Multiset aggregator that splits the guest list into a pre_T bucket (going to the head host T) and a pre_F bucket (going to the tail forest), then aggregates over all remaining assignments. Used to make Ts-Perm-invariance provable by induction on the Perm structure (the swap case becomes a clean Multiset.bind_bind after lifting to the mk-mapped level).

theorem RootedTree.Planar.Pathed.insertionForest_perm_guests {α : Type u_1} (F : List (Planar α)) {Ts Ts' : List (Planar α)} (h : Ts.Perm Ts') : Multiset.map (List.map Nonplanar.mk) (insertionForest F Ts) = Multiset.map (List.map Nonplanar.mk) (insertionForest F Ts')

Forest guest invariance: List.Perm of guests lifts to mk-equality of insertionForest.

§8: Singleton-host insertion = single-tree insertion lifted to singleton lists

insertionForest [T] gs = (insertion T gs).map (fun T' => [T']) — when the host has exactly one tree, the multi-graft is just the single-tree multi-graft with each output wrapped in a singleton list. Used downstream to handle hostTripleSum T [T'] F patterns at the singleton-F_A level.

theorem RootedTree.Planar.Pathed.insertion_nil_guests {α : Type u_1} (T : Planar α) : insertion T [] = {T}

insertion T [] is the singleton {T} — multi-graft of no guests is the identity. Public version of the InsertionAddHost.lean private helper.

theorem RootedTree.Planar.Pathed.insertionForest_singleton {α : Type u_1} (T : Planar α) (gs : List (Planar α)) : insertionForest [T] gs = Multiset.map (fun (T' : Planar α) => [T']) (insertion T gs)

Singleton-host insertion: when the host has exactly one tree, insertionForest reduces to single-tree insertion followed by singleton lift. This lets us match hostTripleSum T [T_other] F patterns by converting (insertionForest [T_other] pre).bind to (insertion T_other pre).bind (via Multiset.bind_map).