Multi-path multi-tree grafting and vertex decomposition for Planar α

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

multiGraft T pairs grafts trees onto T at multiple paths simultaneously, with paths interpreted in the original T (Foissy 2021 convention). The pair list List (Path × Planar α) allows multiple grafts at the same vertex (preserving pair-list order, which matters at the root and at each common host vertex; commutativity at the multiset boundary is upstream in Insertion.lean).

The headline theorem vertices_multiGraft_decomp partitions the path set of multiGraft T pairs into three classes paralleling vertices_insertAt_decomp:

• preserved: vertices of T \ pairSources transported through the cumulative ancestor-source shifts.
• sourceSelf: vertices of T ∩ pairSources (sources of pair grafts), each at its transported original path. Distinct sources contribute multiplicity 1 each — sharing a source does not duplicate the host vertex.
• lifted: for each pair k = (eₖ, Tₖ) and each q ∈ vertices Tₖ, the path transport pairs eₖ ++ posₖ :: q, where posₖ is k's position among pairs sharing source eₖ (in pair-list order, per Foissy 2021 convention).

This decomposition is the vertex-multiset substrate for multi-graft analysis. The deprecated A3.3 basis-level approach to Oudom-Guin Prop 2.7.v has been superseded by the abstract pre-Lie route — see Linglib/Core/Algebra/PreLie/OudomGuinCirc.lean and scratch/pivot_to_prelie_pbw.md.

Specialization to single-pair

multiGraft T [(e, T₂)] = insertAt e T₂ T (multiGraft_singleton), and under that specialization the helpers reduce:

• transport [(e, T₂)] = id on paths disjoint from e's descendants; e ⊏ f → transport [(e, T₂)] f shifts f's child index past e by +1.
• preserveMulti [(e, T₂)] = preserve? e.
• liftMulti [(e, T₂)] ⟨0, _⟩ q = lift e q.

vertices_multiGraft_decomp therefore implies vertices_insertAt_decomp as a corollary (§9).

Design

multiGraftChildren recurses over the children list by shifting path indices rather than carrying an offset:

• pairs starting 0 :: rest are projected to (rest, t) and apply to the current head child;
• pairs starting (k+1) :: rest are projected to (k :: rest, t) and apply to the remaining tail.

The index-shift design simplifies the singleton bridge to insertAt: no arithmetic on offsets, just direct structural cases.

File scope

• §1: Filter helpers (rootPrependFilter, headChildFilter, tailChildFilter).
• §2: multiGraft / multiGraftChildren mutual definitions + simp lemmas.
• §3: Nil identity (multiGraft T [] = T).
• §4: Singleton bridge (multiGraft T [(p, T₂)] = insertAt p T₂ T).
• §5: descentToChild, rootPrependCount — pair-list operations mirroring the multiGraft recursion.
• §6: transport — total path transformer applying cumulative ancestor shifts.
• §7: pairSources, preserveMulti — the preserve-or-drop function.
• §8: posInGroup, liftMulti — the lifted-vertex path embedding.
• §9: vertices_multiGraft_decomp — the headline theorem.
• §10: Single-pair specialization corollaries (depend on §9).

Sibling files:

• Path.lean — Path / IsValidPath / vertices / verticesAux.
• Insert.lean — single-pair insertAt + single-pair vertex decomposition.

Status

[UPSTREAM] candidate. Sorry-free through §10.6, including the descent case of multiGraft_split_lifted_aux (path-arithmetic substrate for A3.3 cons-case Phase 4.2). The headline vertices_multiGraft_decomp (§9) is closed via the §8.5–§8.9 substrate: descent helpers, liftMulti_at_root / liftMulti_at_child_descent, root_bind_eq (root-pair bridge), bind_descent_eq_aux (descent-pair bridge), bind_finRange_singleton_eq (validity-based per-k decomp).

§1: Filter helpers (top-level for matcher stability)

The multiGraft recursion uses three pair-filtering functions: extracting root-prepends (empty path), extracting head-child pairs (first index 0), and shifting tail-child pairs (first index k+1). Each is defined as a top-level function so that all filterMap callers reference the same elaborated matcher — rw with filter equalities then works cleanly across files. Without this, Lean's inline-match elaboration generates fresh match_N aux constants per scope, blocking unification.

Each helper carries unfolding @[simp] lemmas on every pattern so that simp can reduce them where rfl would otherwise fail.

def RootedTree.Planar.Pathed.rootPrependFilter {α : Type u_1} (pair : Path × Planar α) : Option (Planar α)

Extract pair as root prepend iff its path is empty.

Equations

• RootedTree.Planar.Pathed.rootPrependFilter pair = match pair.1 with | [] => some pair.2 | head :: tail => none

@[simp]

theorem RootedTree.Planar.Pathed.rootPrependFilter_of_nil {α : Type u_1} (T : Planar α) : rootPrependFilter ([], T) = some T

@[simp]

theorem RootedTree.Planar.Pathed.rootPrependFilter_of_cons {α : Type u_1} (i : ℕ) (rest : Path) (T : Planar α) : rootPrependFilter (i :: rest, T) = none

def RootedTree.Planar.Pathed.headChildFilter {α : Type u_1} (pair : Path × Planar α) : Option (Path × Planar α)

Extract pair as head-child pair iff its path starts with 0, stripping the leading index.

Equations

• RootedTree.Planar.Pathed.headChildFilter pair = match pair.1 with | 0 :: rest => some (rest, pair.2) | x => none

@[simp]

theorem RootedTree.Planar.Pathed.headChildFilter_of_nil {α : Type u_1} (T : Planar α) : headChildFilter ([], T) = none

@[simp]

theorem RootedTree.Planar.Pathed.headChildFilter_of_zero_cons {α : Type u_1} (rest : Path) (T : Planar α) : headChildFilter (0 :: rest, T) = some (rest, T)

@[simp]

theorem RootedTree.Planar.Pathed.headChildFilter_of_succ_cons {α : Type u_1} (k : ℕ) (rest : Path) (T : Planar α) : headChildFilter ((k + 1) :: rest, T) = none

def RootedTree.Planar.Pathed.tailChildFilter {α : Type u_1} (pair : Path × Planar α) : Option (Path × Planar α)

Extract pair as tail-child pair iff its path starts with k+1, decrementing the leading index by one.

Equations

• RootedTree.Planar.Pathed.tailChildFilter pair = match pair.1 with | k.succ :: rest => some (k :: rest, pair.2) | x => none

@[simp]

theorem RootedTree.Planar.Pathed.tailChildFilter_of_nil {α : Type u_1} (T : Planar α) : tailChildFilter ([], T) = none

@[simp]

theorem RootedTree.Planar.Pathed.tailChildFilter_of_zero_cons {α : Type u_1} (rest : Path) (T : Planar α) : tailChildFilter (0 :: rest, T) = none

@[simp]

theorem RootedTree.Planar.Pathed.tailChildFilter_of_succ_cons {α : Type u_1} (k : ℕ) (rest : Path) (T : Planar α) : tailChildFilter ((k + 1) :: rest, T) = some (k :: rest, T)

§2: multiGraft mutual definition

def RootedTree.Planar.Pathed.multiGraft {α : Type u_1} : Planar α → List (Path × Planar α) → Planar α

multiGraft T pairs: walk T, prepend the trees assigned to each path. Pairs whose path is [] graft at the root (prepended to the children list in pair-list order). Pairs whose path is i :: rest descend into the i-th child with the projected pair (rest, _).

Equations

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

def RootedTree.Planar.Pathed.multiGraftChildren {α : Type u_1} : List (Planar α) → List (Path × Planar α) → List (Planar α)

Auxiliary: descend pair list into children. Pairs with first index 0 apply to the head child (with the rest of the path); pairs with first index k+1 are forwarded to the tail (with the rest of the list and index decremented).

Equations

• One or more equations did not get rendered due to their size.
• RootedTree.Planar.Pathed.multiGraftChildren [] x✝ = []

@[simp]

theorem RootedTree.Planar.Pathed.multiGraft_node {α : Type u_1} (a : α) (cs : List (Planar α)) (pairs : List (Path × Planar α)) : multiGraft (node a cs) pairs = node a (List.filterMap rootPrependFilter pairs ++ multiGraftChildren cs pairs)

@[simp]

theorem RootedTree.Planar.Pathed.multiGraftChildren_nil_cs {α : Type u_1} (pairs : List (Path × Planar α)) : multiGraftChildren [] pairs = []

@[simp]

theorem RootedTree.Planar.Pathed.multiGraftChildren_cons_cs {α : Type u_1} (c : Planar α) (cs : List (Planar α)) (pairs : List (Path × Planar α)) : multiGraftChildren (c :: cs) pairs = multiGraft c (List.filterMap headChildFilter pairs) :: multiGraftChildren cs (List.filterMap tailChildFilter pairs)

§3: Nil identity

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

Empty pair list: multiGraft is the identity.

theorem RootedTree.Planar.Pathed.multiGraftChildren_nil_pairs {α : Type u_1} (cs : List (Planar α)) : multiGraftChildren cs [] = cs

Empty pair list: multiGraftChildren is the identity on the children list.

§4: Singleton bridge to insertAt

A single-pair multiGraft is exactly insertAt. The proof splits into:

• §4.1 multiGraftChildren cs [([], T₂)] = cs — the empty path contributes only to root prepends, not to the children.
• §4.2 multiGraftChildren cs [(j :: rest, T₂)] agrees with cs.set j when j < cs.length, else is the identity.
• §4.3 Top-level multiGraft_singleton combines these.

theorem RootedTree.Planar.Pathed.multiGraft_singleton {α : Type u_1} (T : Planar α) (p : Path) (T₂ : Planar α) : multiGraft T [(p, T₂)] = insertAt p T₂ T

Single-pair multiGraft is insertAt. Bridges the multi-graft primitive to the single-vertex insertion in Insert.lean.

§5: Pair-list operations mirroring multiGraft recursion

multiGraft descends pairs into children via headChildFilter (paths starting with 0) and tailChildFilter (paths starting with k+1). The combined effect on the i-th child is captured by descentToChild i, which keeps pairs whose path begins with i and strips that index.

Root prepends — pairs with empty path — are counted by rootPrependCount, which determines the +N child-index shift seen by every original-T vertex at the current level.

def RootedTree.Planar.Pathed.descentToChild {α : Type u_1} (i : ℕ) : List (Path × Planar α) → List (Path × Planar α)

Filter the pair list to those whose path begins with i, stripping the leading index. The resulting paths address vertices in the i-th child.

Equations

• One or more equations did not get rendered due to their size.
• RootedTree.Planar.Pathed.descentToChild i [] = []
• RootedTree.Planar.Pathed.descentToChild i (([], snd) :: rest) = RootedTree.Planar.Pathed.descentToChild i rest

@[simp]

theorem RootedTree.Planar.Pathed.descentToChild_nil {α : Type u_1} (i : ℕ) : descentToChild i [] = []

@[simp]

theorem RootedTree.Planar.Pathed.descentToChild_cons_nilPath {α : Type u_1} (i : ℕ) (T : Planar α) (rest : List (Path × Planar α)) : descentToChild i (([], T) :: rest) = descentToChild i rest

theorem RootedTree.Planar.Pathed.descentToChild_cons_consPath {α : Type u_1} (i j : ℕ) (rest_p : Path) (T : Planar α) (rest : List (Path × Planar α)) : descentToChild i ((j :: rest_p, T) :: rest) = if i = j then (rest_p, T) :: descentToChild i rest else descentToChild i rest

@[simp]

theorem RootedTree.Planar.Pathed.descentToChild_cons_consPath_eq {α : Type u_1} (i : ℕ) (rest_p : Path) (T : Planar α) (rest : List (Path × Planar α)) : descentToChild i ((i :: rest_p, T) :: rest) = (rest_p, T) :: descentToChild i rest

theorem RootedTree.Planar.Pathed.descentToChild_cons_consPath_ne {α : Type u_1} (i j : ℕ) (rest_p : Path) (T : Planar α) (rest : List (Path × Planar α)) (h : i ≠ j) : descentToChild i ((j :: rest_p, T) :: rest) = descentToChild i rest

def RootedTree.Planar.Pathed.rootPrependCount {α : Type u_1} (pairs : List (Path × Planar α)) : ℕ

Number of pairs whose path is [] — the root-prepend count at the current level. Determines the +N shift of every original-T child index.

Equations

• RootedTree.Planar.Pathed.rootPrependCount pairs = (List.filter (fun (pair : RootedTree.Planar.Pathed.Path × RootedTree.Planar α) => decide (pair.1 = [])) pairs).length

@[simp]

theorem RootedTree.Planar.Pathed.rootPrependCount_nil {α : Type u_1} : rootPrependCount [] = 0

@[simp]

theorem RootedTree.Planar.Pathed.rootPrependCount_cons_nilPath {α : Type u_1} (T : Planar α) (rest : List (Path × Planar α)) : rootPrependCount (([], T) :: rest) = rootPrependCount rest + 1

@[simp]

theorem RootedTree.Planar.Pathed.rootPrependCount_cons_consPath {α : Type u_1} (j : ℕ) (rest_p : Path) (T : Planar α) (rest : List (Path × Planar α)) : rootPrependCount ((j :: rest_p, T) :: rest) = rootPrependCount rest

§6: transport — total path transformer

transport pairs f computes the new path of an original-T vertex f in multiGraft T pairs. Pure path arithmetic; works for any f, even those not in vertices T (no validity hypothesis).

def RootedTree.Planar.Pathed.transport {α : Type u_1} : List (Path × Planar α) → Path → Path

Recursive path transformer: at each level, shift the child index by the root-prepend count, then descend with the projected pair list.

Equations

• RootedTree.Planar.Pathed.transport x✝ [] = []
• RootedTree.Planar.Pathed.transport x✝ (i :: rest) = (i + RootedTree.Planar.Pathed.rootPrependCount x✝) :: RootedTree.Planar.Pathed.transport (RootedTree.Planar.Pathed.descentToChild i x✝) rest

@[simp]

theorem RootedTree.Planar.Pathed.transport_nil_path {α : Type u_1} (pairs : List (Path × Planar α)) : transport pairs [] = []

@[simp]

theorem RootedTree.Planar.Pathed.transport_cons_path {α : Type u_1} (pairs : List (Path × Planar α)) (i : ℕ) (rest : Path) : transport pairs (i :: rest) = (i + rootPrependCount pairs) :: transport (descentToChild i pairs) rest

@[simp]

theorem RootedTree.Planar.Pathed.transport_empty_pairs {α : Type u_1} (f : Path) : transport [] f = f

§7: pairSources, preserveMulti — the preserve-or-drop function

pairSources is the underlying list of pair source paths. preserveMulti returns none on any pair source (excluding it from the preserved class) and some (transport pairs f) otherwise.

def RootedTree.Planar.Pathed.pairSources {α : Type u_1} (pairs : List (Path × Planar α)) : List Path

The list of pair source paths (in pair-list order; may contain duplicates if multiple pairs share a source).

Equations

• RootedTree.Planar.Pathed.pairSources pairs = List.map Prod.fst pairs

@[simp]

theorem RootedTree.Planar.Pathed.pairSources_nil {α : Type u_1} : pairSources [] = []

@[simp]

theorem RootedTree.Planar.Pathed.pairSources_cons {α : Type u_1} (p : Path) (T : Planar α) (rest : List (Path × Planar α)) : pairSources ((p, T) :: rest) = p :: pairSources rest

def RootedTree.Planar.Pathed.preserveMulti {α : Type u_1} (pairs : List (Path × Planar α)) (f : Path) : Option Path

The preserve-or-drop function for the multi-pair case.

• none if f is any pair source (excluded from the preserved class).
• some (transport pairs f) otherwise (transport applies the cumulative ancestor-source shifts).

Mirrors preserve? for the single-pair case.

Equations

• RootedTree.Planar.Pathed.preserveMulti pairs f = if f ∈ RootedTree.Planar.Pathed.pairSources pairs then none else some (RootedTree.Planar.Pathed.transport pairs f)

@[simp]

theorem RootedTree.Planar.Pathed.preserveMulti_empty {α : Type u_1} (f : Path) : preserveMulti [] f = some f

§7.5: A3.3 substrate — preserved + sourceSelf = vertices.map transport

The preserved-class filterMap (preserveMulti pairs) and the sourceSelf-class filter (∈ pairSources) .map (transport pairs) partition vertices T by membership in pairSources pairs. Combined, they cover all of vertices T, each mapped under transport pairs.

theorem RootedTree.Planar.Pathed.filterMap_preserveMulti_eq_filter_map_transport {α : Type u_1} (pairs : List (Path × Planar α)) (vs : Multiset Path) : Multiset.filterMap (preserveMulti pairs) vs = Multiset.map (transport pairs) (Multiset.filter (fun (x : Path) => ¬x ∈ pairSources pairs) vs)

filterMap (preserveMulti pairs) decomposes as filter (∉ pairSources) composed with map (transport pairs). Direct from the if-none-else-some shape of preserveMulti.

theorem RootedTree.Planar.Pathed.preserved_add_sourceSelf_eq_vertices_map_transport {α : Type u_1} (pairs : List (Path × Planar α)) (vs : Multiset Path) : Multiset.filterMap (preserveMulti pairs) vs + Multiset.map (transport pairs) (Multiset.filter (fun (x : Path) => x ∈ pairSources pairs) vs) = Multiset.map (transport pairs) vs

The preserved + sourceSelf classes of vertices (multiGraft T pairs) together equal vertices T mapped under transport pairs.

§8: posInGroup, liftMulti — lifted-vertex paths

For pair k = (eₖ, Tₖ), vertices q ∈ vertices Tₖ lift to transport pairs eₖ ++ posₖ :: q, where posₖ is k's 0-indexed position among pairs targeting eₖ (in pair-list order). When all pairs have distinct sources, every posₖ = 0.

def RootedTree.Planar.Pathed.posInGroup {α : Type u_1} (pairs : List (Path × Planar α)) (k : Fin pairs.length) : ℕ

Position of pair k among pairs sharing the same source path (counting only earlier pairs in pair-list order).

Equations

• RootedTree.Planar.Pathed.posInGroup pairs k = (List.filter (fun (pair : RootedTree.Planar.Pathed.Path × RootedTree.Planar α) => decide (pair.1 = pairs[k].1)) (List.take (↑k) pairs)).length

def RootedTree.Planar.Pathed.liftMulti {α : Type u_1} (pairs : List (Path × Planar α)) (k : Fin pairs.length) (q : Path) : Path

The path of vertex q ∈ vertices (pairs[k].snd) in multiGraft T pairs.

Equations

• RootedTree.Planar.Pathed.liftMulti pairs k q = RootedTree.Planar.Pathed.transport pairs pairs[k].1 ++ RootedTree.Planar.Pathed.posInGroup pairs k :: q

§8.5: Substrate lemmas for the decomposition

Five identities needed by the main proof:

1. length_filterMap_rootPrependFilter: the rootPrepends list has length equal to rootPrependCount pairs.
2. descentToChild_zero: descentToChild 0 pairs = pairs.filterMap headChildFilter.
3. descentToChild_succ: descentToChild (i+1) pairs = descentToChild i (pairs.filterMap tailChildFilter).
4. descent_pairSources_iff: rest ∈ pairSources (descentToChild i pairs) ↔ (i :: rest) ∈ pairSources pairs.
5. preserveMulti_cons: preserveMulti pairs (i :: rest) = (preserveMulti (descentToChild i pairs) rest).map ((i + rootPrependCount pairs) :: ·).

These bridge the multiGraft recursion (on filterMap headChildFilter / tailChildFilter) to the path-arithmetic operations (descentToChild, rootPrependCount, transport).

@[simp]

theorem RootedTree.Planar.Pathed.length_filterMap_rootPrependFilter {α : Type u_1} (pairs : List (Path × Planar α)) : (List.filterMap rootPrependFilter pairs).length = rootPrependCount pairs

Length of the root-prepends list equals rootPrependCount.

theorem RootedTree.Planar.Pathed.descentToChild_zero {α : Type u_1} (pairs : List (Path × Planar α)) : descentToChild 0 pairs = List.filterMap headChildFilter pairs

descentToChild 0 pairs agrees with pairs.filterMap headChildFilter.

theorem RootedTree.Planar.Pathed.descentToChild_succ {α : Type u_1} (i : ℕ) (pairs : List (Path × Planar α)) : descentToChild (i + 1) pairs = descentToChild i (List.filterMap tailChildFilter pairs)

descentToChild (i+1) pairs agrees with descending into the i-th child of pairs.filterMap tailChildFilter. The shift (k+1) :: rest ↦ k :: rest on tail-child paths exactly cancels the +1 in the descent index.

theorem RootedTree.Planar.Pathed.descent_pairSources_iff {α : Type u_1} (i : ℕ) (rest : Path) (pairs : List (Path × Planar α)) : rest ∈ pairSources (descentToChild i pairs) ↔ i :: rest ∈ pairSources pairs

A path rest is a source of the descended pair list iff i :: rest is a source of the original pair list.

theorem RootedTree.Planar.Pathed.preserveMulti_cons {α : Type u_1} (pairs : List (Path × Planar α)) (i : ℕ) (rest : Path) : preserveMulti pairs (i :: rest) = Option.map (fun (x : List ℕ) => (i + rootPrependCount pairs) :: x) (preserveMulti (descentToChild i pairs) rest)

The decomposition of preserveMulti over a cons path: descending into child i strips the leading i and shifts the next index by the rootPrependCount.

theorem RootedTree.Planar.Pathed.mem_descentToChild_iff {α : Type u_1} (i : ℕ) (rest : Path) (T : Planar α) (pairs : List (Path × Planar α)) : (rest, T) ∈ descentToChild i pairs ↔ (i :: rest, T) ∈ pairs

Membership in descentToChild i pairs — a pair (rest, T) appears iff the original (i :: rest, T) appears in pairs. The .snd is preserved under descent; the .fst loses its leading i.

theorem RootedTree.Planar.Pathed.descentToChild_valid_of_node {α : Type u_1} (a : α) (cs : List (Planar α)) (pairs : List (Path × Planar α)) (h_valid : ∀ (pair : Path × Planar α), pair ∈ pairs → IsValidPath pair.1 (node a cs)) (i : Fin cs.length) (pair : Path × Planar α) : pair ∈ descentToChild (↑i) pairs → IsValidPath pair.1 cs[↑i]

Per-child validity: if every pair source is valid in node a cs, then every descended pair (under child i) has its source valid in cs[i]. Used by the main vertices_multiGraft_decomp proof to derive the IH hypothesis on each child.

§8.6: Children-block companion lemma

The main theorem's structural decomposition needs a companion lemma giving the per-child unfolding of verticesAux N (multiGraftChildren cs pairs). This is mutually recursive with the main theorem (the companion calls main on each cs[i], which is structurally smaller than node a cs).

§8.7: Helpers for the 3-class decomposition proof

Three helpers needed by the headline proof:

1. verticesAux_unfold: the no-graft companion of verticesAux_multiGraftChildren_unfold — verticesAux offset cs as a bind over child indices. Specializes the multi-graft version with pairs = [].
2. preserveMulti_cons_post_map: pointwise bridge identifying (preserveMulti (descentToChild i pairs) f).map ((i + N) :: ·) with preserveMulti pairs (i :: f). Uses preserveMulti_cons.
3. transport_descent_via_cons: pointwise bridge identifying transport (descentToChild i pairs) f (after prepending) with transport pairs (i :: f). Uses transport_cons_path.

§8.8: Bijection helpers for the lifted bridge (step 8)

The (i, k') ↔ k bijection between descent-indexed pairs and original pairs. Built around descentCount (a counting form of descentToChild i pairs's length) and descentIdxOf (the descent-corresponding index function).

Properties needed by step 8:

• descentToChild_length_eq: (descentToChild i pairs).length = descentCount i pairs.
• descentToChild_take: walking-the-prefix gives a prefix-of-the-walk.
• descentToChild_getElem: characterizes (descentToChild i pairs)[k'].
• descentIdxOf_lt: validity of descentIdxOf as a Fin-index.
• posInGroup_descent_invariance: posInGroup is preserved under descent.

The bijection is implicit; step 8 uses these properties to re-organize the LHS bind to match RHS via Multiset.bind_congr after transport_cons_descent.

§8.9: Step-8 lifted bridge — bijection on bind indices

Step 8 of vertices_multiGraft_decomp is a multiset equation between two re-indexings of the same family of "lifted" vertex contributions:

LHS = ↑(verticesAux 0 rootPrepends) + bind_{i : Fin n} (head-shift ∘ bind_{k' : descentToChild i pairs} liftMulti) RHS = bind_{k : Fin pairs.length} liftMulti pairs k ∘ ↑vertices pairs[k].snd

Strategy: split RHS into root-pair and child-pair contributions via Multiset.filter_add_not + add_bind, then identify each half with the corresponding LHS part:

• Root half. For k with pairs[k].fst = [], liftMulti pairs k q = posInGroup pairs k :: q. By induction on pairs, the root-pair bind equals ↑(verticesAux 0 rootPrepends).
• Child half. For k with pairs[k].fst = i :: rest, liftMulti pairs k q = (N + i) :: liftMulti (descent i pairs) ⟨descentIdxOf i pairs k, _⟩ q (via posInGroup_descent_invariance + descentToChild_getElem_at_descentIdxOf). By induction on pairs, the head-i slice equals map ((N+i)::·) (bind_{k'} ...). Summing over i ∈ Fin cs.length recovers LHS Part 2 under the validity hypothesis.

Root-pair bridge

The conditional bind over Fin pairs.length-indices, contributing (vertices pairs[k].snd).map ((offset + posInGroup pairs k) :: ·) for root pairs (and 0 otherwise), equals ↑(verticesAux offset rootPrepends). Strengthened with offset to support induction on pairs.

Descent-pair bridge

The conditional bind over Fin pairs.length-indices, contributing F ⟨descentIdxOf i pairs k, _⟩ exactly when pairs[k].fst.head? = some i, equals the bind over Fin (descentToChild i pairs).length of the same F. Parameterized by an external n (instead of (descentToChild i pairs).length) to dodge the dependent-rewrite trap when recursing on pairs: in sub-case B (i = j head), the recursive call needs to produce an F' of type Fin n' → Multiset β for n' = n - 1, which is impossible if F's type is tied to a pairs-dependent expression. Threading n as an independent parameter and h_len as the identification lets the recursion in B re-bind F' cleanly. The sole caller passes (descentToChild i.val pairs).length and rfl.

Indicator-singleton bind helper

Bind over Fin n of a value-conditional indicator (matching one specific j < n) collapses to the value. Used in step 8's per-k validity decomposition: when a child pair has head j < cs.length, exactly one i ∈ Fin cs.length matches.

[UPSTREAM] candidate: this is the Multiset.bind analogue of mathlib's Finset.sum_ite_eq (Algebra/BigOperators/Group/Finset/Piecewise.lean). The cleaner factoring goes through two missing mathlib lemmas: a generic Multiset.bind_ite (s.bind (fun a => if p a then f a else 0) = (s.filter p).bind f) plus (List.finRange n).filter (· = ⟨j, h⟩) = [⟨j, h⟩]. Both are real gaps.

§8.10: stripLiftMulti — operational inverse of liftMulti

The map liftMulti pairs k injects vertices q ∈ vertices pairs[k].snd into the lifted-class image at transport pairs pairs[k].fst ++ (posInGroup pairs k :: q). stripLiftMulti is an Option-valued operational inverse: it returns some q exactly when the input path matches that shape.

The aux walker stripLiftMultiAux e posIG outer p traces e step by step, checking at each level that the input path's head matches the expected rootPrependCount-offsetted descent index. Recursion is structural on e.

Consumer (§11.5, composePairs_planarEquiv_partition): the partition of inner paths into "lifted at outer[k]" buckets vs "root vertices of the extended tree" uses stripLiftMulti as the filter discriminator.

def RootedTree.Planar.Pathed.stripLiftMultiAux {α : Type u_1} : Path → ℕ → List (Path × Planar α) → Path → Option Path

Auxiliary walker: structural recursion on the prefix path.

Equations

• One or more equations did not get rendered due to their size.
• RootedTree.Planar.Pathed.stripLiftMultiAux [] x✝¹ x✝ [] = none
• RootedTree.Planar.Pathed.stripLiftMultiAux [] x✝¹ x✝ (h :: q) = if h = x✝¹ then some q else none
• RootedTree.Planar.Pathed.stripLiftMultiAux (head :: tail) x✝¹ x✝ [] = none

def RootedTree.Planar.Pathed.stripLiftMulti {α : Type u_1} (pairs : List (Path × Planar α)) (k : Fin pairs.length) (p : Path) : Option Path

Operational inverse of liftMulti: stripLiftMulti pairs k p = some q iff p = liftMulti pairs k q. Computable.

Equations

• RootedTree.Planar.Pathed.stripLiftMulti pairs k p = RootedTree.Planar.Pathed.stripLiftMultiAux pairs[↑k].1 (RootedTree.Planar.Pathed.posInGroup pairs k) pairs p

theorem RootedTree.Planar.Pathed.stripLiftMultiAux_eq_some_iff {α : Type u_1} (e : Path) (posIG : ℕ) (outer : List (Path × Planar α)) (p q : Path) : stripLiftMultiAux e posIG outer p = some q ↔ p = transport outer e ++ posIG :: q

Characterization of stripLiftMultiAux: it returns some q exactly when the input path equals transport outer e ++ (posIG :: q). Proof by structural induction on e.

theorem RootedTree.Planar.Pathed.stripLiftMulti_eq_some_iff {α : Type u_1} (pairs : List (Path × Planar α)) (k : Fin pairs.length) (p q : Path) : stripLiftMulti pairs k p = some q ↔ p = liftMulti pairs k q

Iff-characterization: stripLiftMulti pairs k p = some q exactly when p is the lifted image of q under liftMulti pairs k.

theorem RootedTree.Planar.Pathed.stripLiftMulti_liftMulti {α : Type u_1} (pairs : List (Path × Planar α)) (k : Fin pairs.length) (q : Path) : stripLiftMulti pairs k (liftMulti pairs k q) = some q

Correctness: stripping a lifted vertex recovers the original.

§8.11: untransport — operational inverse of transport

transport pairs v computes the path of v ∈ vertices T in multiGraft T pairs. untransport pairs p returns some v if p = transport pairs v for some v, else none. Used in §11.5 rootInner to recover T-coordinate paths from preserved/sourceSelf inner vertices.

def RootedTree.Planar.Pathed.untransport {α : Type u_1} : List (Path × Planar α) → Path → Option Path

Recursive Option-valued inverse of transport: strips the rootPrependCount-offset at each level, recursing into descended pairs.

Equations

• One or more equations did not get rendered due to their size.
• RootedTree.Planar.Pathed.untransport x✝ [] = some []

@[simp]

theorem RootedTree.Planar.Pathed.untransport_nil {α : Type u_1} (outer : List (Path × Planar α)) : untransport outer [] = some []

theorem RootedTree.Planar.Pathed.untransport_eq_some_iff {α : Type u_1} (outer : List (Path × Planar α)) (p v : Path) : untransport outer p = some v ↔ p = transport outer v

Iff-characterization: untransport outer p = some v iff p = transport outer v. Proof by structural induction on p.

theorem RootedTree.Planar.Pathed.untransport_transport {α : Type u_1} (outer : List (Path × Planar α)) (v : Path) : untransport outer (transport outer v) = some v

Correctness: untransporting a transported vertex recovers the original.

§9: The decomposition theorem

The 3-class decomposition statement. Proof is the headline of A3.0 phase 2.

The substrate identities (§8.5–§8.8) are sorry-free. The singleton corollaries (§10) follow as direct consequences.

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

Multi-pair decomposition lemma. Under the validity hypothesis that every pair's source is a valid path in T, the vertex multiset of multiGraft T pairs partitions into:

1. preserved: (vertices T).filterMap (preserveMulti pairs) — non-source T-vertices, each transported.
2. sourceSelf: source vertices of T (those whose path is in pairSources pairs), each transported.
3. lifted: for each pair k and each q ∈ vertices (pairs[k].snd), the path liftMulti pairs k q.

Specializes to vertices_insertAt_decomp for single-pair lists (corollary in §10).

§9.5: Corollary — transport pairs v_T ∈ vertices (multiGraft T pairs)

Direct consequence of vertices_multiGraft_decomp + the §7.5 identity that the preserved + sourceSelf classes equal vertices T mapped under transport pairs. Consumed by A3.3 substrate multiGraft_compose_cons_pair_at_choice to discharge the v_c ∈ vertices T' hypothesis when v_c is a transported T-vertex.

theorem RootedTree.Planar.Pathed.transport_mem_vertices_multiGraft {α : Type u_1} (T : Planar α) (pairs : List (Path × Planar α)) (h_valid : ∀ (pair : Path × Planar α), pair ∈ pairs → IsValidPath pair.1 T) (v_T : Path) (h_v_T : v_T ∈ vertices T) : transport pairs v_T ∈ vertices (multiGraft T pairs)

For any vertex v_T ∈ vertices T, the transported path transport pairs v_T is a vertex of multiGraft T pairs.

§10: Single-pair specialization corollaries

When pairs = [(e, T₂)], the multi-pair decomposition reduces to vertices_insertAt_decomp. Validates the API shape against the existing substrate.

theorem RootedTree.Planar.Pathed.transport_singleton_self {α : Type u_1} (e : Path) (T₂ : Planar α) : transport [(e, T₂)] e = e

Singleton transport on the source itself: transport [(e, T₂)] e = e. The source path is at every level shifted by 0 (the only pair contributes to descent, never to root-prepends, except at the end where it's an empty descent).

theorem RootedTree.Planar.Pathed.transport_singleton_of_ne {α : Type u_1} (e : Path) (T₂ : Planar α) (f : Path) (_hne : f ≠ e) : transport [(e, T₂)] f = preserveOf e f

Single-pair transport agrees with preserveOf for f ≠ e. The diagonal is captured by preserveMulti = preserve? (see preserveMulti_singleton).

theorem RootedTree.Planar.Pathed.preserveMulti_singleton {α : Type u_1} (e : Path) (T₂ : Planar α) (f : Path) : preserveMulti [(e, T₂)] f = preserve? e f

preserveMulti [(e, T₂)] = preserve? e. Combines transport_singleton_of_ne (off-diagonal) with preserve?_self (diagonal).

theorem RootedTree.Planar.Pathed.liftMulti_singleton {α : Type u_1} (e : Path) (T₂ : Planar α) (q : Path) : liftMulti [(e, T₂)] ⟨0, ⋯⟩ q = lift e q

liftMulti [(e, T₂)] ⟨0, _⟩ q = lift e q. The single pair's posInGroup is 0 (no earlier same-source pairs) and its transported source is e itself (transport_singleton_self).

§10.5: Forest-aux companion to vertices_multiGraft_decomp

The forest-aux companion gives the per-child 3-class decomposition of verticesAux N (multiGraftChildren cs pairs). Composes verticesAux_multiGraftChildren_unfold (per-child unfolding via descentToChild) with vertices_multiGraft_decomp (per-tree 3-class decomposition).

This is Phase 3.1 substrate for the A3.3 cons-case proof (scratch/a33_cons_plan.md). Consumers (Phase 4) further distribute the .map ((offset + i.val) :: ·) over the 3-class sum at the use site.

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

Forest-aux companion to vertices_multiGraft_decomp. The vertices of verticesAux offset (multiGraftChildren cs pairs) decompose, per-child i, into the same 3-class sum as for a single tree (preserved / sourceSelf / lifted), with the per-child paths prepended by (offset + i.val). The validity hypothesis is supplied per-child via descentToChild.

theorem RootedTree.Planar.Pathed.vertices_forest_eq_partition {α : Type u_1} (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 : ℕ) : ↑(verticesAux offset (List.map (fun (i : Fin cs.length) => multiGraft cs[↑i] (per_tree_pairs i)) (List.finRange cs.length))) = (↑(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))

Forest-level partition of vertices for an arbitrary list of multiGraft results. Generalizes verticesAux_multiGraftChildren_decomp: instead of a single pair list with descent into children, each tree cs[i] is grafted against its own pair list per_tree_pairs i. The grafted forest is constructed via (List.finRange cs.length).map fun i => multiGraft cs[i] _, and its verticesAux offset decomposes per-tree into the 3-class partition (preserved / sourceSelf / lifted), with each class prepended by (offset + i.val).

This is the substrate Phase 4 of the A3.3 cons-case proof (scratch/a33_cons_plan.md) consumes when decomposing vertices(T_ins :: F_ins) into the 4-class V-partition by QuadIdx.

§10.6: multiGraft_split_lifted_aux — single-graft commutation

Grafting c at a lifted-vertex position liftMulti pairs k q in multiGraft T pairs equals multi-grafting T with pairs.set k.val (pairs[k.val].fst, insertAt q c pairs[k.val].snd). The single-graft baby version of the full multiGraft_compose (Route B, ~600+ LOC).

Substrate for Phase 4.2 of the A3.3 cons-case proof (scratch/a33_cons_plan.md): "graft C-element at a T_graft-bucket vertex of T_ins" equals "first insert C-element into the corresponding pre_T_B subtree, then graft the modified pre_T_B-list into T". Per-c application; multiple T_graft-routed C-elements iterate via the q-relative-to-modified-subtree update.

§10.6.1 Helper: posInGroup of a root pair is < rootPrependCount

§10.6.2 Helpers for the root case

The next two helpers (rootPrepends_at_posInGroup_eq_snd and filterMap_rootPrepend_set_root) both reduce to structural induction on pairs with case analysis on p.fst and k_val. The arithmetic is straightforward but the proofs require care with dependent-type rewrites (the goal has arr[posInGroup ...]'h where the proof h depends on posInGroup).

§10.6.3 Helpers for the descent case

§10.6.4 Helpers for the descent-case set commutation

§10.6.5 Main statement

theorem RootedTree.Planar.Pathed.multiGraft_split_lifted_aux {α : Type u_1} (T : Planar α) (pairs : List (Path × Planar α)) (k : Fin pairs.length) (q : Path) (c : Planar α) : insertAt (liftMulti pairs k q) c (multiGraft T pairs) = multiGraft T (pairs.set ↑k (pairs[↑k].1, insertAt q c pairs[↑k].2))

Single-graft baby version of multiGraft composition: grafting c at a lifted-vertex path of multiGraft T pairs equals multi-grafting T with pair k modified to have c inserted into its tree at relative path q.

This is the path-arithmetic substrate for Phase 4.2 of the A3.3 cons-case proof (scratch/a33_cons_plan.md). Single-graft only; multi-graft variants iterate this via the q-relative-to-modified-subtree update.

Proof: structural induction on T = Planar.node a cs.

• Case (a) pairs[k.val].fst = []: liftMulti = posInGroup k :: q. Both sides land at the posInGroup k-th rootPrepend, modified to insertAt q c pairs[k.val].snd.
• Case (b) pairs[k.val].fst = j :: rest: by liftMulti_at_child_descent the lifted path is (rootPrependCount pairs + j) :: liftMulti (descentToChild j pairs) k' q. The LHS descends past root-prepends into the j-th element of multiGraftChildren cs pairs (= multiGraft cs[j] (descentToChild j pairs)) and applies the IH on cs[j]. The RHS is reassembled via multiGraftChildren_set_same_head (or _invalid_head when j ≥ cs.length, where both sides are no-ops).

§10.7: multiGraft_cons_pair — preserved-vertex multiGraft-extend

Prepending a new pair (v, c) to the pair list equals inserting c at the transported path of v in multiGraft T pairs. The "preserved" analog of multiGraft_split_lifted_aux (§10.6), but in PREPEND form rather than APPEND form — this avoids the planar-order mismatch at the root (where insertAt [] c puts c first in children but multiGraft T (pairs ++ [([], c)]) puts c last in root-prepends).

Why prepend form works without a validity hypothesis.

• v = [] case: both sides yield node a (c :: rootPrepends ++ multiGraftChildren); the new ([], c) pair is the first root-prepend, matching insertAt [] c's prepend-to-children semantics.
• v = j :: rest, j < cs.length case: descend into the j-th child via the IH (decreasing on the child's weight); the (rest, c) descented pair is the first in the child's pair list.
• v = j :: rest, j ≥ cs.length case: both sides are no-ops (multiGraftChildren ignores the new pair since no valid descent target; insertAt is a no-op past the children-list bound).

The APPEND form multiGraft T (pairs ++ [(v, c)]) follows from this lemma plus multiGraft_perm_pair (only at PlanarEquiv level, since planar-order differs between prepend and append at root).

This is the substrate for Phase D (T_orig and FA_orig buckets) of A3.3's cons-case proof (scratch/a33_phase4_2_session_prompt_16.md).

theorem RootedTree.Planar.Pathed.multiGraft_cons_pair {α : Type u_1} (T : Planar α) (pairs : List (Path × Planar α)) (v : Path) (c : Planar α) : multiGraft T ((v, c) :: pairs) = insertAt (transport pairs v) c (multiGraft T pairs)

Prepend form: prepending (v, c) to the pair list equals inserting c at the transported path of v in multiGraft T pairs. No validity hypothesis on v: out-of-bounds case is a mutual no-op.

The "preserved" analog of multiGraft_split_lifted_aux (§10.6). Phase A substrate for A3.3's cons-case proof (scratch/a33_phase4_2_session_prompt_16.md).

§11: multiGraft_compose — full nested multi-graft composition

Status (2026-05-15, 0.231.79): plan landed; substrate not yet built. See scratch/multigraft_compose_plan.md for full specification.

Statement:

theorem multiGraft_compose (T : Planar α)
    (outer_pairs : List (Path × Planar α))
    (inner_pairs : List (Path × Planar α))
    (h_outer_valid : ∀ p ∈ outer_pairs, IsValidPath p.fst T)
    (h_inner_valid : ∀ p ∈ inner_pairs, IsValidPath p.fst (multiGraft T outer_pairs)) :
    multiGraft (multiGraft T outer_pairs) inner_pairs =
    multiGraft T (composePairs outer_pairs inner_pairs)

Why needed: Closes A3.3 helpers LHS_TRUE_eq_T_buckets / LHS_FALSE_eq_FA_buckets (substantive Phase 2-4 of each). The LHS contains nested multi-grafts mG T' (...) where T' = mG T outer_pairs; collapsing to a single multi-graft mG T composed_pairs enables matching the RHS T_orig / T_graft / FA_orig / FA_graft summands.

composePairs semantics: for each inner pair (p, c) at position p ∈ vertices (mG T outer_pairs):

• preserved/sourceSelf (p = transport outer_pairs v for v ∈ vertices T): add (v, c) to outer_pairs.
• lifted (p = liftMulti outer_pairs k q): modify outer_pairs[k].snd to insertAt q c outer_pairs[k].snd.

These three classes are exhaustive by vertices_multiGraft_decomp (§9).

Proof structure (~600 LOC across 3-4 sessions):

• Phase A (~150 LOC): composePairs definition (operational via decodePath decoder) + theorem statement.
• Phase B (~150 LOC): inner_pairs = [] base case + cons-step setup via multiGraft_cons_pair.
• Phase C (~200 LOC): per-class handling in cons step (preserved/sourceSelf via multiGraft_cons_pair; lifted via multiGraft_split_lifted_aux).
• Phase D (~100 LOC): termination (decreasing weight argument).

Substrate consumed: vertices_multiGraft_decomp (§9), multiGraft_cons_pair (§10.7), multiGraft_split_lifted_aux (§10.6), transport / liftMulti / pairSources / preserveMulti (§7-8).

§11.1: absorbInnerPair — single inner-pair absorption

For an inner pair (p, c) where p ∈ vertices (mG T outer), returns the modified outer pair list whose multi-graft of T equals insertAt p c (mG T outer).

Three-class semantics (by vertices_multiGraft_decomp):

• preserved (p = transport outer v, v ∉ pairSources): (v, c) :: outer (PREPEND)
• sourceSelf (p = transport outer v, v ∈ pairSources): (v, c) :: outer (PREPEND)
• lifted (p = liftMulti outer k q): outer.set k.val (..., insertAt q c outer[k].snd)

PREPEND, not APPEND (subtle planar-order issue): the LHS mG (mG T outer) inner puts inner root prepends FIRST in the result tree's children (followed by outer's children). For the RHS to match planar-equally, cp.filterMap rootPrependFilter must be inner_root_prepends ++ outer_root_prepends, i.e., NEW pairs go to the FRONT of the pair list. APPEND would give outer_root_prepends ++ inner_root_prepends (wrong order, planar-FALSE). See [[feedback_multigraft_compose_prepend_foldr]].

Implementation strategy (recursive descent on p's structure relative to rootPrependCount outer):

• If p = []: PREPEND ([], c) to outer.
• If p = i :: rest, i < rootPrependCount outer: lifted in outer's i-th root prepend → modify outer.set k where k = rootPrependPairIdx outer i.
• If p = i :: rest, i ≥ rootPrependCount outer: descend into T's (i - rootPrependCount outer)-th child; recurse on descented outer pairs; lift back via liftBackToOuter.

Returns the original outer unchanged on invalid inputs (defensive).

def RootedTree.Planar.Pathed.rootPrependPairIdx {α : Type u_1} (outer : List (Path × Planar α)) : ℕ → Option (Fin outer.length)

Find the pair-list index k whose pair contributes the i-th root-prepend (i.e., the (i+1)-th pair in pair-list order with .fst = []). Returns none if i ≥ rootPrependCount outer.

Recursive on the outer list (as opposed to a filter over List.finRange): avoids dependent-type issues when proving recursive equation lemmas.

Equations

• RootedTree.Planar.Pathed.rootPrependPairIdx [] x✝ = none
• RootedTree.Planar.Pathed.rootPrependPairIdx (([], snd) :: rest) 0 = some 0
• RootedTree.Planar.Pathed.rootPrependPairIdx (([], snd) :: rest) i.succ = Option.map Fin.succ (RootedTree.Planar.Pathed.rootPrependPairIdx rest i)
• RootedTree.Planar.Pathed.rootPrependPairIdx ((head :: tail, snd) :: rest) x✝ = Option.map Fin.succ (RootedTree.Planar.Pathed.rootPrependPairIdx rest x✝)

§11.1.5: rootPrependPairIdx totality + bridge lemma

rootPrependPairIdx_ne_none_of_lt gives totality: when i < rootPrependCount outer, the result is some _. The bridge lemma posInGroup_of_rootPrependPairIdx relates the returned Fin index to posInGroup, used in the lifted-at-root subcase of absorbInnerPair_eq_insertAt.

def RootedTree.Planar.Pathed.liftBackToOuter {α : Type u_1} (descented modified : List (Path × Planar α)) (j : ℕ) (outer : List (Path × Planar α)) : List (Path × Planar α)

Lift a modification of descented = descentToChild j outer back to a modification of outer. Two cases by length:

• modified.length = descented.length + 1: PREPEND case at descented level. modified = (q, T) :: descented for some (q, T). Lift back: prepend (j :: q, T) to outer.
• modified.length = descented.length: SET case at descented level. Walk through outer, substituting .snd at j-headed pair positions with corresponding modified positions (no-op at non-modified positions).

Equations

• One or more equations did not get rendered due to their size.
• RootedTree.Planar.Pathed.liftBackToOuter descented [] j outer = if [].length = descented.length + 1 then outer else RootedTree.Planar.Pathed.walkAndReplace✝ j outer [] 0

@[irreducible]

def RootedTree.Planar.Pathed.absorbInnerPair {α : Type u_1} (outer : List (Path × Planar α)) (p : Path) (c : Planar α) : List (Path × Planar α)

Absorb a single inner pair (p, c) into outer, returning the modified pair list. Recursive on path structure:

• p = []: root vertex (preserved/sourceSelf class, v = []). PREPEND ([], c) to outer.
• p = i :: rest, i < rootPrependCount outer: lifted at pair k. Modify outer[k] to insert c at rest in outer[k].snd.
• p = i :: rest, i ≥ rootPrependCount outer: descend into T's child at index (i - rootPrependCount outer). Recurse on the descended outer pairs, then lift back via liftBackToOuter.

Equations

• One or more equations did not get rendered due to their size.
• RootedTree.Planar.Pathed.absorbInnerPair outer [] c = ([], c) :: outer

§11.1.6: walkAndReplace and liftBackToOuter substrate

Properties used in the descent case of absorbInnerPair_eq_insertAt.

§11.1.7: absorbInnerPair equation lemmas + length dichotomy

Equation lemmas for the SET-at-root and descent cases of absorbInnerPair, plus the length dichotomy: result length is X.length or X.length + 1.

§11.1.8: walkAndReplace and liftBackToOuter correctness lemmas

§11.1.9: liftBackToOuter structural properties

§11.2: composePairs — full inner-list composition

Composes inner pairs into outer via right-fold (foldr) with transport-based path re-addressing. Each inner pair (p, c) has p as a vertex of the original mG T outer; after composing the rest, the position of p in mG T (composePairs outer rest) = mG (mG T outer) rest is transport rest p. The re-addressing is essential for the cons-case proof of multiGraft_compose.

Why foldr (not foldl): The leftmost inner pair must be absorbed LAST (so that its empty-path PREPEND ends up FIRST in the result list — matching the planar order of root prepends in the LHS mG (mG T outer) inner). foldl + PREPEND would reverse inner-order; foldr + PREPEND preserves it.

def RootedTree.Planar.Pathed.composePairs {α : Type u_1} : List (Path × Planar α) → List (Path × Planar α) → List (Path × Planar α)

Equations

• One or more equations did not get rendered due to their size.
• RootedTree.Planar.Pathed.composePairs x✝ [] = x✝

@[simp]

theorem RootedTree.Planar.Pathed.composePairs_nil {α : Type u_1} (outer : List (Path × Planar α)) : composePairs outer [] = outer

@[simp]

theorem RootedTree.Planar.Pathed.composePairs_cons {α : Type u_1} (outer : List (Path × Planar α)) (p : Path) (c : Planar α) (rest : List (Path × Planar α)) : composePairs outer ((p, c) :: rest) = absorbInnerPair (composePairs outer rest) (transport rest p) c

§11.3: absorbInnerPair_eq_insertAt — singleton case

The singleton case of multiGraft_compose: absorbing one inner pair into outer gives the same result as inserting at the corresponding position.

mG T (absorbInnerPair outer p c) = insertAt p c (mG T outer)

This holds (as PLANAR equality, no validity hypothesis) by case analysis on p:

• p = []: by multiGraft_cons_pair at (T, outer, [], c) — both sides reduce to insertAt [] c (mG T outer).
• p = i :: rest, i < N: by multiGraft_split_lifted_aux plus the identity liftMulti outer k rest = i :: rest (which holds via liftMulti_at_root + posInGroup_of_rootPrependPairIdx bridge).
• p = i :: rest, i ≥ N (descent): by recursion on rest (smaller path), with liftBackToOuter's structural properties (_filterMap_rootPrepend, _descentToChild_self, _descentToChild_other) bridging the modified outer back to the multiGraft of the original. Invalid descent (j ≥ cs.length) is a no-op on both sides.

@[simp]

theorem RootedTree.Planar.Pathed.absorbInnerPair_nil_path {α : Type u_1} (outer : List (Path × Planar α)) (c : Planar α) : absorbInnerPair outer [] c = ([], c) :: outer

Equation lemma: empty-path case of absorbInnerPair.

theorem RootedTree.Planar.Pathed.absorbInnerPair_eq_insertAt {α : Type u_1} (T : Planar α) (outer : List (Path × Planar α)) (p : Path) (c : Planar α) : multiGraft T (absorbInnerPair outer p c) = insertAt p c (multiGraft T outer)

The singleton case of multiGraft_compose. Stated unconditionally (no validity hypothesis); the empty-path case holds without validity, the lifted-at-root case via multiGraft_split_lifted_aux + the bridge posInGroup_of_rootPrependPairIdx, and the descent case via IH on rest + liftBackToOuter correctness (descentToChild_self/other, filterMap_rootPrepend).

§11.4: multiGraft_compose — main theorem

theorem RootedTree.Planar.Pathed.multiGraft_compose {α : Type u_1} (T : Planar α) (outer_pairs inner_pairs : List (Path × Planar α)) (_h_outer_valid : ∀ (p : Path × Planar α), p ∈ outer_pairs → IsValidPath p.1 T) (h_inner_valid : ∀ (p : Path × Planar α), p ∈ inner_pairs → IsValidPath p.1 (multiGraft T outer_pairs)) : multiGraft (multiGraft T outer_pairs) inner_pairs = multiGraft T (composePairs outer_pairs inner_pairs)

Nested multi-graft composition. Collapses a multi-graft of a multi-graft into a single multi-graft of the original host with composed pairs.

Proof structure: induction on inner_pairs. Cons case uses multiGraft_cons_pair to peel the head, IH to convert the inner mG of T, composePairs_cons to unfold the RHS, then absorbInnerPair_eq_insertAt to close.

Currently depends on absorbInnerPair_eq_insertAt (§11.3) being closed.

§11.5: liftedInnerAt, rootInner — partition extractors

For an outer pair list and inner pair list (with inner paths valid in mG T outer), the 3-class decomposition (§9 vertices_multiGraft_decomp) classifies each inner path into one of:

• lifted at outer[k]: p = liftMulti outer k q for some q. Recovered by stripLiftMulti outer k p = some q (§8.10).
• preserved/sourceSelf: p = transport outer v for some v ∈ vertices T. Recovered by untransport outer p = some v (§8.11).

liftedInnerAt outer inner k collects the lifted-at-k inner pairs as (q, c) (stripped paths). rootInner outer inner collects the preserved/sourceSelf inner pairs as (v, c) (untransported paths).

The partition theorem composePairs_planarEquiv_partition lives in Insertion.lean §5.6 (uses Nonplanar.mk from Linglib.Core.Combinatorics.RootedTree.Nonplanar).

Consumer status (2026-05-16): deprecated. The original consumer (InsertionAssoc.lean §1.11.11 T-bucket bridges) has been deleted as the project pivoted to the abstract pre-Lie route. These helpers remain as generic vertex-decomposition primitives; revive if a future basis- level analysis needs them.

noncomputable def RootedTree.Planar.Pathed.liftedInnerAt {α : Type u_1} (outer inner : List (Path × Planar α)) (k : Fin outer.length) : List (Path × Planar α)

Inner pairs lifted at outer[k], with paths stripped to outer[k].snd vertices.

Equations

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

noncomputable def RootedTree.Planar.Pathed.rootInner {α : Type u_1} (outer inner : List (Path × Planar α)) : List (Path × Planar α)

Inner pairs in the preserved/sourceSelf class, with paths untransported back to T-coordinates.

Equations

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

@[simp]

theorem RootedTree.Planar.Pathed.liftedInnerAt_nil {α : Type u_1} (outer : List (Path × Planar α)) (k : Fin outer.length) : liftedInnerAt outer [] k = []

@[simp]

theorem RootedTree.Planar.Pathed.rootInner_nil {α : Type u_1} (outer : List (Path × Planar α)) : rootInner outer [] = []

theorem RootedTree.Planar.Pathed.liftedInnerAt_cons {α : Type u_1} (outer : List (Path × Planar α)) (p : Path × Planar α) (rest : List (Path × Planar α)) (k : Fin outer.length) : liftedInnerAt outer (p :: rest) k = (Option.map (fun (x : Path) => (x, p.2)) (stripLiftMulti outer k p.1)).toList ++ liftedInnerAt outer rest k

theorem RootedTree.Planar.Pathed.rootInner_cons {α : Type u_1} (outer : List (Path × Planar α)) (p : Path × Planar α) (rest : List (Path × Planar α)) : rootInner outer (p :: rest) = (Option.map (fun (x : Path) => (x, p.2)) (untransport outer p.1)).toList ++ rootInner outer rest