Cut-avoiding trees in the nonplanar Connes–Kreimer coproduct

[MCB25] [Foi02]

A pure structural condition on Nonplanar α: when does a tree T avoid a target X? Answer: T ≠ X and no Δ^ρ cut summand of T extracts X as a crown component — equivalently, no summand of' M ⊗ ofTree R of the deletion coproduct Δ^ρ T has X ∈ M.

This is the cutSummandsN-based re-derivation of the legacy CutAvoiding (stated over CutShape/TraceTree in Core/Combinatorics/RootedTree/CutAvoiding.lean), matching the n-ary cut-multiset shape. The predicate is generic over the leaf alphabet α and has nothing to do with any particular linguistic theory; it is a relation between trees in the Connes–Kreimer combinatorial substrate.

Contents

• CutAvoidingN X T: per-target, per-tree predicate.
• CutAvoidingForestN F W: per-target-forest, per-workspace predicate (every component of W avoids every element of F).
• Namespace lemmas: CutAvoidingForestN.{empty, of_cons, head, not_mem, no_cut, head_pair, not_mem_pair}.

Consumed by Minimalist.Merge.mergeOp_factor_out_singleton / mergeOp_pair_residual (MCB Lemma 1.4.1 Case 1).

structure RootedTree.ConnesKreimer.CutAvoidingN {α : Type u_1} (X T : 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 : Forest (Nonplanar α) × Nonplanar α) : p ∈ cutSummandsN T → X ∉ p.1

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

def RootedTree.ConnesKreimer.CutAvoidingForestN {α : Type u_1} (F W : Forest (Nonplanar α)) : Prop

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

Equations

• RootedTree.ConnesKreimer.CutAvoidingForestN F W = ∀ T ∈ W, ∀ X ∈ F, RootedTree.ConnesKreimer.CutAvoidingN X T

theorem RootedTree.ConnesKreimer.CutAvoidingForestN.empty {α : Type u_1} (F : Forest (Nonplanar α)) : CutAvoidingForestN F 0

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

theorem RootedTree.ConnesKreimer.CutAvoidingForestN.of_cons {α : Type u_1} {F W : Forest (Nonplanar α)} {T : Nonplanar α} (h : CutAvoidingForestN F (T ::ₘ W)) : CutAvoidingForestN F W

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

theorem RootedTree.ConnesKreimer.CutAvoidingForestN.head {α : Type u_1} {F W : Forest (Nonplanar α)} {T : Nonplanar α} (h : CutAvoidingForestN F (T ::ₘ W)) (X : Nonplanar α) : X ∈ F → CutAvoidingN X T

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

theorem RootedTree.ConnesKreimer.CutAvoidingForestN.not_mem {α : Type u_1} {F W : Forest (Nonplanar α)} (h : CutAvoidingForestN F W) (X : Nonplanar α) : X ∈ F → X ∉ W

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

theorem RootedTree.ConnesKreimer.CutAvoidingForestN.no_cut {α : Type u_1} {F W : Forest (Nonplanar α)} (h : CutAvoidingForestN F W) (T : Nonplanar α) : T ∈ W → ∀ X ∈ F, ∀ 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.

theorem RootedTree.ConnesKreimer.CutAvoidingForestN.head_pair {α : Type u_1} {S S' T : Nonplanar α} {W : Forest (Nonplanar α)} (h : CutAvoidingForestN {S, S'} (T ::ₘ W)) : CutAvoidingN S T ∧ CutAvoidingN S' T

For a workspace T ::ₘ W avoiding the pair-target forest {S, S'}, extract both per-tree avoidances at T. Convenience for the two-operand Merge case.

theorem RootedTree.ConnesKreimer.CutAvoidingForestN.not_mem_pair {α : Type u_1} {S S' : Nonplanar α} {W : Forest (Nonplanar α)} (h : CutAvoidingForestN {S, S'} W) : S ∉ W ∧ S' ∉ W

For a workspace W avoiding the pair-target forest {S, S'}, neither target is a member of W. Convenience for the two-operand Merge case.