Path-based single-vertex insertion and vertex decomposition for Planar α

@cite{foissy-typed-decorated-rooted-trees-2018} @cite{chapoton-livernet-2001}

insertAt p T₂ T grafts T₂ as a new first child at the vertex addressed by path p in T. Out-of-bounds path: no-op.

The headline theorem vertices_insertAt_decomp partitions the path set of Pathed.insertAt e t₂ t₁ into three classes:

• preserved: paths of t₁ \ {e} transported through the insertion (a child-index shift when e is a proper prefix).
• sourceSelf: the source vertex e itself (still present in the post-graft tree, just with a new first child).
• lifted: paths of t₂ embedded under e (each q ∈ vertices t₂ ends up at path e ++ 0 :: q since t₂ is grafted at child index 0).

This decomposition is the substrate behind the pre-Lie identity in Algebra.lean: each (insertAt v t₂) ◁ t₃ splits into three sums, each of which has a clean cancellation against a symmetric counterpart.

The path-form is flat, non-dependent: preserveOf e f, lift e q, etc. are pure path manipulations that don't carry T or T₂ in their types. IsValidPath obligations are discharged per-theorem with explicit hypotheses.

File scope

• §1: insertAt — single-vertex graft primitive.
• §2: lift, newGraft — embedding t₂-paths into the post-graft tree.
• §3: sourceSelf — the source vertex's path post-graft.
• §4: preserve?, preserveOf — transporting a non-source vertex.
• §5: Commutativity insertAt_commute_diff and lifted-equals-nested insertAt_lift_eq_nested.
• §6: Multiset decomposition vertices_insertAt_decomp.
• §7: Preserved-class swap bind_filterMap_preserve?_swap.

Sibling files:

• Path.lean — Path / IsValidPath / vertices / verticesAux.
• Graft.lean — multi-pair multiGraft + multi-pair vertex decomposition.

Status

[UPSTREAM] candidate. Sorry-free, no noncomputable.

§1: insertAt

def RootedTree.Planar.Pathed.insertAt {α : Type u_1} : Path → Planar α → Planar α → Planar α

Insert T₂ as a new first child at the vertex addressed by path p in T. Returns T unchanged if p is out of bounds (no-op fallback for invalid paths).

Equations

• One or more equations did not get rendered due to their size.
• RootedTree.Planar.Pathed.insertAt [] x✝ (RootedTree.Planar.node a cs) = RootedTree.Planar.node a (x✝ :: cs)

@[simp]

theorem RootedTree.Planar.Pathed.insertAt_nil {α : Type u_1} (T₂ : Planar α) (a : α) (cs : List (Planar α)) : insertAt [] T₂ (node a cs) = node a (T₂ :: cs)

@[simp]

theorem RootedTree.Planar.Pathed.insertAt_cons_of_lt {α : Type u_1} (i : ℕ) (rest : Path) (T₂ : Planar α) (a : α) (cs : List (Planar α)) (h : i < cs.length) : insertAt (i :: rest) T₂ (node a cs) = node a (cs.set i (insertAt rest T₂ cs[i]))

theorem RootedTree.Planar.Pathed.insertAt_cons_of_not_lt {α : Type u_1} (i : ℕ) (rest : Path) (T₂ : Planar α) (a : α) (cs : List (Planar α)) (h : ¬i < cs.length) : insertAt (i :: rest) T₂ (node a cs) = node a cs

§2: lift, newGraft — embedding T₂ into the post-graft tree

When T₂ is grafted at path e in T, T₂'s root is at path e ++ [0], and a vertex of T₂ at internal path q ends up at e ++ 0 :: q.

def RootedTree.Planar.Pathed.lift (e q : Path) : Path

The position in Pathed.insertAt e t₂ T of the vertex q ∈ T₂.

Equations

• RootedTree.Planar.Pathed.lift e q = e ++ 0 :: q

@[simp]

theorem RootedTree.Planar.Pathed.lift_def (e q : Path) : lift e q = e ++ 0 :: q

@[simp]

theorem RootedTree.Planar.Pathed.lift_nil_left (q : Path) : lift [] q = 0 :: q

def RootedTree.Planar.Pathed.newGraft (e : Path) : Path

The position of T₂'s root in Pathed.insertAt e t₂ T.

Equations

• RootedTree.Planar.Pathed.newGraft e = e ++ [0]

@[simp]

theorem RootedTree.Planar.Pathed.newGraft_eq_lift_nil (e : Path) : newGraft e = lift e []

§3: sourceSelf — the source vertex's path post-graft

The vertex at path e in T is still at path e in Pathed.insertAt e t₂ T — it didn't move, it just gained a new first child. The path-form analogue of Vertex.sourceSelf is the identity on e.

def RootedTree.Planar.Pathed.sourceSelf (e : Path) : Path

The position of the source vertex e in the post-graft tree. Just e.

Equations

• RootedTree.Planar.Pathed.sourceSelf e = e

@[simp]

theorem RootedTree.Planar.Pathed.sourceSelf_def (e : Path) : sourceSelf e = e

§4: preserve?, preserveOf — transporting a non-source vertex

Given paths e f in T with f ≠ e, what's f's path in Pathed.insertAt e t₂ T? Four cases on the prefix relation of e and f:

• e = f: diagonal, none.
• f is a strict ancestor of e: f unchanged.
• e is a strict ancestor of f: f = e ++ (j :: rest) shifts to e ++ ((j+1) :: rest) (new child t₂ at index 0 pushes original children up).
• e f branch at some common ancestor: f unchanged.

def RootedTree.Planar.Pathed.preserve? : Path → Path → Option Path

Total Option-valued preservation: none on the diagonal, some of the shifted path elsewhere. Pure path arithmetic (no T, no T₂).

Equations

• RootedTree.Planar.Pathed.preserve? [] [] = none
• RootedTree.Planar.Pathed.preserve? [] (j :: rest) = some ((j + 1) :: rest)
• RootedTree.Planar.Pathed.preserve? (head :: tail) [] = some []
• RootedTree.Planar.Pathed.preserve? (i :: rest_e) (j :: rest_f) = if i = j then Option.map (fun (x : List ℕ) => i :: x) (RootedTree.Planar.Pathed.preserve? rest_e rest_f) else some (j :: rest_f)

@[simp]

theorem RootedTree.Planar.Pathed.preserve?_nil_nil : preserve? [] [] = none

@[simp]

theorem RootedTree.Planar.Pathed.preserve?_nil_cons (j : ℕ) (rest : Path) : preserve? [] (j :: rest) = some ((j + 1) :: rest)

@[simp]

theorem RootedTree.Planar.Pathed.preserve?_cons_nil (i : ℕ) (rest : Path) : preserve? (i :: rest) [] = some []

theorem RootedTree.Planar.Pathed.preserve?_cons_cons (i j : ℕ) (rest_e rest_f : Path) : preserve? (i :: rest_e) (j :: rest_f) = if i = j then Option.map (fun (x : List ℕ) => i :: x) (preserve? rest_e rest_f) else some (j :: rest_f)

@[simp]

theorem RootedTree.Planar.Pathed.preserve?_self (e : Path) : preserve? e e = none

Diagonal: preserve? e e = none.

def RootedTree.Planar.Pathed.preserveOf : Path → Path → Path

Off-diagonal: when f ≠ e, preserve? e f is some _. The path is given by preserveOf below.

Equations

• RootedTree.Planar.Pathed.preserveOf [] [] = []
• RootedTree.Planar.Pathed.preserveOf [] (j :: rest) = (j + 1) :: rest
• RootedTree.Planar.Pathed.preserveOf (head :: tail) [] = []
• RootedTree.Planar.Pathed.preserveOf (i :: rest_e) (j :: rest_f) = if i = j then i :: RootedTree.Planar.Pathed.preserveOf rest_e rest_f else j :: rest_f

@[simp]

theorem RootedTree.Planar.Pathed.preserveOf_nil_cons (j : ℕ) (rest : Path) : preserveOf [] (j :: rest) = (j + 1) :: rest

@[simp]

theorem RootedTree.Planar.Pathed.preserveOf_cons_nil (i : ℕ) (rest : Path) : preserveOf (i :: rest) [] = []

theorem RootedTree.Planar.Pathed.preserveOf_cons_cons (i j : ℕ) (rest_e rest_f : Path) : preserveOf (i :: rest_e) (j :: rest_f) = if i = j then i :: preserveOf rest_e rest_f else j :: rest_f

theorem RootedTree.Planar.Pathed.preserve?_of_ne (e f : Path) (_h : f ≠ e) : preserve? e f = some (preserveOf e f)

Off-diagonal: preserve? e f = some (preserveOf e f) when f ≠ e.

§5: Commutativity + lifted-equals-nested

Two algebraic identities about Pathed.insertAt that drive the pre-Lie identity proof in Algebra.lean.

theorem RootedTree.Planar.Pathed.insertAt_commute_diff {α : Type u_1} (e f : Path) (_h : f ≠ e) (t₁ t₂ t₃ : Planar α) : insertAt (preserveOf e f) t₃ (insertAt e t₂ t₁) = insertAt (preserveOf f e) t₂ (insertAt f t₃ t₁)

Commutativity at distinct paths: inserting t₂ at e then t₃ at the f-image equals inserting t₃ at f then t₂ at the e-image. The (e, f) ↔ (f, e) re-keying lives in preserveOf.

Proof structure: case-analyze the prefix relation of e and f, recurse on the shared prefix. Four primary cases:

• Both empty: contradicts h.
• e = [], f = j :: rest_f: insert at root, child shift.
• e = i :: rest_e, f = []: symmetric.
• Both non-empty: branch on i = j (recurse) vs i ≠ j (different child slots, commute via List.set_comm).

Within each non-empty case, sub-case on index < cs.length (in bounds — meaningful insertion) vs out-of-bounds (both no-op).

theorem RootedTree.Planar.Pathed.insertAt_lift_eq_nested {α : Type u_1} (e : Path) (t₁ t₂ t₃ : Planar α) (q : Path) : insertAt (lift e q) t₃ (insertAt e t₂ t₁) = insertAt e (insertAt q t₃ t₂) t₁

Lifted-equals-nested: inserting t₃ at a lifted vertex of t₂ (lifted into Pathed.insertAt e t₂ t₁) factors as insertAt e (insertAt q t₃ t₂).

Pure path arithmetic, no IsValidPath hypotheses needed — the no-op fallback of Pathed.insertAt handles invalid paths uniformly on both sides.

§6: Multiset decomposition of vertices (insertAt e t₂)

The 3-class decomposition: every path in insertAt e t₂ t₁ is either preserved (from t₁ \ {e}), the source e itself, or lifted (from t₂). Stated as a Multiset equality with explicit RHS summands.

This is the substrate behind the pre-Lie identity proof in Algebra.lean (§4): each (insertAt v t₂) ◁ t₃ splits into three sums, each of which has a clean cancellation against a symmetric counterpart.

Substrate: shift lemma for filterMap (preserve? [])

Substrate: list-set decomposition for verticesAux

Substrate: filterMap (preserve? (i :: rest)) away from i

theorem RootedTree.Planar.Pathed.vertices_insertAt_decomp {α : Type u_1} (e : Path) (t₁ t₂ : Planar α) (_he : IsValidPath e t₁) : ↑(vertices (insertAt e t₂ t₁)) = Multiset.filterMap (preserve? e) ↑(vertices t₁) + {sourceSelf e} + Multiset.map (lift e) ↑(vertices t₂)

The decomposition lemma in path form. Assumes e is a valid path in t₁. The preserved class uses filterMap preserve? e (skipping e itself); sourceSelf is the singleton {e}; lifted is map (lift e) (vertices t₂).

§7: Preserved-class swap

The (e, f) ↔ (f, e) symmetry for preserved-class double sums. Used by assoc_symm_planar to identify the preserved class of (t₁ ◁ t₂) ◁ t₃ with the preserved class of (t₁ ◁ t₃) ◁ t₂.

The pointwise bridge is insertAt_commute_diff: at distinct paths e ≠ f of t₁, grafting t₂ at e then t₃ at the f-image equals grafting t₃ at f then t₂ at the e-image. The diagonal e = f is discarded by preserve?_self = none on both sides.

theorem RootedTree.Planar.Pathed.bind_filterMap_preserve?_swap {α : Type u_1} (t₁ t₂ t₃ : Planar α) : ((↑(vertices t₁)).bind fun (e : Path) => Multiset.filterMap (fun (f : Path) => Option.map (fun (pos : Path) => insertAt pos t₃ (insertAt e t₂ t₁)) (preserve? e f)) ↑(vertices t₁)) = (↑(vertices t₁)).bind fun (e : Path) => Multiset.filterMap (fun (f : Path) => Option.map (fun (pos : Path) => insertAt pos t₂ (insertAt e t₃ t₁)) (preserve? e f)) ↑(vertices t₁)