Single-tree pre-Lie product insertSum on Planar α and Nonplanar α

@cite{foissy-typed-decorated-rooted-trees-2018} @cite{chapoton-livernet-2001} @cite{marcolli-chomsky-berwick-2025}

The vertex-grafting pre-Lie product on planar / nonplanar n-ary rooted trees: for trees T₁, T₂, T₁ ◁ T₂ is the multiset of all trees obtained by grafting T₂ as a new child of some vertex of T₁:

T₁ ◁ T₂ = Σ_{v ∈ V(T₁)} graft(v, T₁, T₂)

This file contains both the planar definition (Foissy 2018 Prop 2.2, Chapoton-Livernet) and its descent through Nonplanar.mk to the nonplanar carrier.

Reference

@cite{foissy-typed-decorated-rooted-trees-2018} Proposition 2.2 defines the multiple pre-Lie product on D-decorated T-typed rooted trees (D = decoration set, T = edge type set). Specialized to T = {*} (single edge type) and decoration set α, this is exactly insertSum.

@cite{chapoton-livernet-2001} introduced the original CL pre-Lie product on undecorated rooted trees, of which the present construction is the decorated extension.

Relation to MCB §1.7

@cite{marcolli-chomsky-berwick-2025} Definition 1.7.1 (book p. 77) defines a DIFFERENT pre-Lie product on nonplanar BINARY rooted trees with leaf labels in SO_0 (internal vertices unlabeled), via edge subdivision. The two are distinct algebras on distinct carriers — neither is a specialization of the other. Both satisfy the abstract pre-Lie identity (mathlib's RightPreLieAlgebra); a future binary substrate file would add a separate RightPreLieAlgebra instance for MCB §1.7.

File scope

• §1: insertSum planar definition + simp lemmas + leaf case.
• §2: Cardinality (card_insertSum_eq_weight).
• §3: Decomposition (insertSum_eq_coe_map_insertAt).
• §4: Cardinality consistency.
• §5: Cons-decomposition projection helpers (descent §1).
• §6: Right invariance (PlanarEquiv on T₂).
• §7: List-side perm + componentwise PlanarEquiv invariance.
• §8: Left invariance (PlanarEquiv on T₁).
• §9: EqvGen lift to PlanarEquiv on either argument.
• §10: Native Nonplanar.insertSum via Quotient.lift₂.
• §11: Quotient-unfolding lemma + Nonplanar cardinality.
• §12: Sanity tests.

Sibling files:

• Path.lean / Insert.lean — path-based vertex enumeration + grafting (Pathed.vertices, Pathed.insertAt).
• Insertion.lean — multi-tree multi-vertex grafting (Foissy 2021).
• VertexBijection.lean — vertex classification + commutativity.
• Algebra.lean — RightPreLieAlgebra ℤ instance.

insertSum — the vertex-grafting product

Mutually recursive on (Planar, List Planar) mirroring weight / weightList etc. Each summand of insertSum T₁ T₂ corresponds to a choice of vertex v in T₁; the corresponding tree replaces v's children list cs with T₂ :: cs.

def RootedTree.Planar.insertSum {α : Type u_1} : Planar α → Planar α → Multiset (Planar α)

The pre-Lie product T₁ ◁ T₂ on Planar α (vertex grafting): the multiset of all trees obtained by grafting T₂ as a new child of some vertex of T₁.

Equations

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

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

Auxiliary: graft T₂ inside one of the entries of a children list, returning the multiset of resulting children-lists (one per vertex inside the list).

Equations

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

def RootedTree.Planar.«term_◁_» : Lean.TrailingParserDescr

Notation T₁ ◁ T₂ for insertSum T₁ T₂. The right-triangular Unicode glyph matches Foissy's typesetting. Scoped to avoid clashing with mathlib's LeftPreLieRing notation.

Equations

• RootedTree.Planar.«term_◁_» = Lean.ParserDescr.trailingNode `RootedTree.Planar.«term_◁_» 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ◁ ") (Lean.ParserDescr.cat `term 66))

@[simp]

theorem RootedTree.Planar.insertSum_node {α : Type u_1} (a : α) (cs : List (Planar α)) (T₂ : Planar α) : (node a cs).insertSum T₂ = node a (T₂ :: cs) ::ₘ Multiset.map (fun (cs' : List (Planar α)) => node a cs') (insertSumList cs T₂)

@[simp]

theorem RootedTree.Planar.insertSumList_nil {α : Type u_1} (T₂ : Planar α) : insertSumList [] T₂ = 0

@[simp]

theorem RootedTree.Planar.insertSumList_cons {α : Type u_1} (c : Planar α) (cs : List (Planar α)) (T₂ : Planar α) : insertSumList (c :: cs) T₂ = Multiset.map (fun (c' : Planar α) => c' :: cs) (c.insertSum T₂) + Multiset.map (fun (cs' : List (Planar α)) => c :: cs') (insertSumList cs T₂)

@[simp]

theorem RootedTree.Planar.insertSum_leaf {α : Type u_1} (a : α) (T₂ : Planar α) : (leaf a).insertSum T₂ = {node a [T₂]}

A leaf has exactly one summand: graft T₂ at the root.

Cardinality — card (T₁ ◁ T₂) = T₁.weight

Each vertex of T₁ contributes one summand. Proved by mutual structural induction mirroring the definition.

theorem RootedTree.Planar.card_insertSum_eq_weight {α : Type u_1} (T₁ T₂ : Planar α) : (T₁.insertSum T₂).card = T₁.weight

The number of summands in T₁ ◁ T₂ equals T₁.weight (total vertex count).

theorem RootedTree.Planar.card_insertSumList_eq_weightList {α : Type u_1} (cs : List (Planar α)) (T₂ : Planar α) : (insertSumList cs T₂).card = weightList cs

The number of children-lists in insertSumList cs T₂ equals weightList cs (sum of weights of entries).

Decomposition — insertSum via Pathed.vertices + Pathed.insertAt

Bridge lemma between the recursive (Multiset) formulation of insertSum in §1 and the per-path (List) formulation in Path.lean / Insert.lean. The lemma is the basis for the pre-Lie identity proof in Algebra.lean: each summand of insertSum T₁ T₂ is uniquely identified by a path into T₁.

theorem RootedTree.Planar.insertSum_eq_coe_map_insertAt {α : Type u_1} (T₁ T₂ : Planar α) : T₁.insertSum T₂ = ↑(List.map (fun (p : Pathed.Path) => Pathed.insertAt p T₂ T₁) (Pathed.vertices T₁))

Decomposition lemma: T₁ ◁ T₂ equals the multiset of Pathed.insertAt p T₂ T₁ for p ranging over Pathed.vertices T₁.

theorem RootedTree.Planar.insertSumList_eq_coe_map_pathInsertAt_aux {α : Type u_1} (a : α) (pre cs : List (Planar α)) (T₂ : Planar α) : Multiset.map (fun (cs' : List (Planar α)) => node a (pre ++ cs')) (insertSumList cs T₂) = ↑(List.map (fun (p : Pathed.Path) => Pathed.insertAt p T₂ (node a (pre ++ cs))) (Pathed.verticesAux pre.length cs))

Auxiliary: with pre siblings before the cs-tail being grafted in, children-list grafting through pre-prefixed Planar.node a equals the path-based insertions at offset pre.length into the original host Planar.node a (pre ++ cs).

Cardinality consistency

The two cardinality computations agree: (T₁ ◁ T₂).card = (Pathed.vertices T₁).length.

theorem RootedTree.Planar.card_insertSum_eq_length_vertices {α : Type u_1} (T₁ T₂ : Planar α) : (T₁.insertSum T₂).card = (Pathed.vertices T₁).length

Descent of insertSum through Nonplanar.mk

The descent layer: lift Planar.insertSum to Nonplanar α via Quotient.lift₂, requiring invariance under PlanarEquiv on both arguments. Mirrors the original PreLie/Nonplanar.lean pre-restructure.

Cons-decomposition of insertSumList-projection

Helper lemma used by both §6 right-invariance and §7 list permutation proofs. The cons case of insertSumList cs T₂ splits into a per-head grafting (in insertSum c T₂) plus a per-tail grafting (in insertSumList tail T₂); after projection through mk ∘ node a, the two halves are clean two-summand decompositions with simpler wrappers than the raw Multiset.map_map form.

Right invariance — T₂ → T₂'

If T₂ ≡ T₂' (PlanarEquiv), then (T₁ ◁ T₂).map mk = (T₁ ◁ T₂').map mk for any T₁. Mutually inducted with the children-list version insertSumList.

theorem RootedTree.Nonplanar.insertSum_planarEquiv_right {α : Type u_1} (T₁ : Planar α) {T₂ T₂' : Planar α} (h : T₂.PlanarEquiv T₂') : Multiset.map mk (T₁.insertSum T₂) = Multiset.map mk (T₁.insertSum T₂')

Right invariance for insertSum.

List-side mk-projection of insertSumList

Two key properties of (insertSumList cs T₂).map (mk ∘ .node a): Perm-invariance in cs and componentwise PlanarEquiv-invariance.

Left invariance — T₁ → T₁' via PlanarStep induction

theorem RootedTree.Nonplanar.insertSum_planarStep_left {α : Type u_1} {T₁ T₁' : Planar α} (h : T₁.PlanarStep T₁') (T₂ : Planar α) : Multiset.map mk (T₁.insertSum T₂) = Multiset.map mk (T₁'.insertSum T₂)

Left invariance for insertSum under a single PlanarStep on T₁.

EqvGen lift to PlanarEquiv

theorem RootedTree.Nonplanar.insertSum_planarEquiv_left {α : Type u_1} {T₁ T₁' : Planar α} (h : T₁.PlanarEquiv T₁') (T₂ : Planar α) : Multiset.map mk (T₁.insertSum T₂) = Multiset.map mk (T₁'.insertSum T₂)

Left invariance under PlanarEquiv on T₁. Standard EqvGen recipe.

Native Nonplanar.insertSum via Quotient.lift₂

def RootedTree.Nonplanar.insertSum {α : Type u_1} : Nonplanar α → Nonplanar α → Multiset (Nonplanar α)

The vertex-grafting pre-Lie product on Nonplanar α: lifted from the planar Planar.insertSum via Quotient.lift₂, using the invariance lemmas from §6 and §9.

Equations

• RootedTree.Nonplanar.insertSum = Quotient.lift₂ (fun (t₁ t₂ : RootedTree.Planar α) => Multiset.map RootedTree.Nonplanar.mk (t₁.insertSum t₂)) ⋯

def RootedTree.Nonplanar.«term_◁_» : Lean.TrailingParserDescr

Notation T₁ ◁ T₂ for Nonplanar.insertSum T₁ T₂. Scoped to the Nonplanar namespace to coexist with the planar ◁.

Equations

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

Quotient-unfolding lemma + Nonplanar cardinality

@[simp]

theorem RootedTree.Nonplanar.mk_insertSum {α : Type u_1} (t₁ t₂ : Planar α) : (mk t₁).insertSum (mk t₂) = Multiset.map mk (t₁.insertSum t₂)

Quotient unfolding: Nonplanar.insertSum (mk t₁) (mk t₂) is the multiset of nonplanar grafting summands obtained by projecting the planar grafting summands.

theorem RootedTree.Nonplanar.card_insertSum_eq_weight {α : Type u_1} (T₁ T₂ : Nonplanar α) : (T₁.insertSum T₂).card = T₁.weight

The number of summands of T₁ ◁ T₂ equals T₁.weight, i.e., the nonplanar tree-vertex count of T₁.

Sanity tests at compile time