Cut-avoiding trees

[MCB25] [Foi02]

A tree T avoids a target X when T ≠ X and no Δ^ρ cut summand of T extracts X as a crown component (CutAvoiding), together with the componentwise closure to forests (CutAvoidingForest).

structure ConnesKreimer.CutAvoiding {α : Type u_1} (X T : RoseTree.Nonplanar α) : Prop

A tree T avoids the target X in the nonplanar Δ^ρ coproduct: T ≠ X and no cut summand of T extracts X as a crown component. Equivalently, no summand of' M ⊗ ofTree R of Δ^ρ T has X ∈ M.

• ne_self : T ≠ X

  T is not literally the target X.

• no_cut (p : Multiset (RoseTree.Nonplanar α) × RoseTree.Nonplanar α) : p ∈ cutSummandsN T → ¬X ∈ p.1

  No cut summand of T has X in its crown forest.

theorem ConnesKreimer.cutAvoiding_iff {α : Type u_1} (X T : RoseTree.Nonplanar α) : CutAvoiding X T ↔ T ≠ X ∧ ∀ (p : Multiset (RoseTree.Nonplanar α) × RoseTree.Nonplanar α), p ∈ cutSummandsN T → ¬X ∈ p.1

def ConnesKreimer.CutAvoidingForest {α : Type u_1} (F W : Multiset (RoseTree.Nonplanar α)) : Prop

A workspace W : Multiset (Nonplanar α) is F-avoiding (component-wise): every component T of W avoids every target X in the forest F.

Equations

• ConnesKreimer.CutAvoidingForest F W = ∀ (T : RoseTree.Nonplanar α), T ∈ W → ∀ (X : RoseTree.Nonplanar α), X ∈ F → ConnesKreimer.CutAvoiding X T

theorem ConnesKreimer.CutAvoidingForest.empty {α : Type u_1} (F : Multiset (RoseTree.Nonplanar α)) : CutAvoidingForest F 0

Empty workspace is trivially F-avoiding for any target forest F.

theorem ConnesKreimer.CutAvoidingForest.of_cons {α : Type u_1} {F W : Multiset (RoseTree.Nonplanar α)} {T : RoseTree.Nonplanar α} (h : CutAvoidingForest F (T ::ₘ W)) : CutAvoidingForest F W

Cons preservation: if T ::ₘ W is F-avoiding then so is W.

theorem ConnesKreimer.CutAvoidingForest.head {α : Type u_1} {F W : Multiset (RoseTree.Nonplanar α)} {T : RoseTree.Nonplanar α} (h : CutAvoidingForest F (T ::ₘ W)) (X : RoseTree.Nonplanar α) : X ∈ F → CutAvoiding X T

Cons head: if T ::ₘ W is F-avoiding then T avoids every X ∈ F.

theorem ConnesKreimer.CutAvoidingForest.not_mem {α : Type u_1} {F W : Multiset (RoseTree.Nonplanar α)} (h : CutAvoidingForest F W) (X : RoseTree.Nonplanar α) : X ∈ F → ¬X ∈ W

Workspace-level: no target X ∈ F is a member of the workspace W.

theorem ConnesKreimer.CutAvoidingForest.no_cut {α : Type u_1} {F W : Multiset (RoseTree.Nonplanar α)} (h : CutAvoidingForest F W) (T : RoseTree.Nonplanar α) : T ∈ W → ∀ (X : RoseTree.Nonplanar α), X ∈ F → ∀ (p : Multiset (RoseTree.Nonplanar α) × RoseTree.Nonplanar α), p ∈ cutSummandsN T → ¬X ∈ p.1

Workspace-level: no cut summand of any component T ∈ W extracts any target X ∈ F as a crown component.