⚠️ LEGACY — RESTORED SHIM (2026-05-13)

Restored from commit e0876460^ after deletion at 0.230.913. Consumer migration (Phase D per scratch/mcb_full_architecture.md) hadn't happened. Will be re-deleted when Phase D lands — predicates here will be re-derived on the new substrate (cutSummandsCP / Planar (α ⊕ β)), matching the new cut-multiset shape rather than the old per-tree CutShape type.

Do not extend, do not add new consumers.

---

Cut-avoiding trees in the Connes-Kreimer coproduct

@cite{marcolli-chomsky-berwick-2025} @cite{foissy-2002}

A pure structural condition on TraceTree α β: when does a tree T "avoid" a target X? Answer: T ≠ X and no admissible cut on T extracts X as a subforest element. Equivalently — interpreted in the Connes-Kreimer Hopf algebra — no summand M ⊗ R of the deletion coproduct Δ^d T has X ∈ M.

This predicate has nothing to do with any particular linguistic theory; it is a relation between trees in the Connes-Kreimer combinatorial substrate. Generic over leaf alphabet α and trace alphabet β. Defined here so that any consumer (Minimalism-style algebraic Merge per @cite{marcolli-chomsky-berwick-2025}, TAG-via-Hopf, categorial-grammar combinators, renormalization-style "avoid these counterterms") can reuse it.

Contents

• CutAvoiding X T: per-target, per-tree predicate.
• CutAvoidingForest F W: per-target-forest, per-workspace predicate (every component of W avoids every element of F).
• Namespace lemmas: CutAvoidingForest.empty, CutAvoidingForest.of_cons, CutAvoidingForest.head, CutAvoidingForest.not_mem, CutAvoidingForest.no_cut.

structure ConnesKreimer.CutAvoiding {α : Type u_1} {β : Type u_2} (X T : TraceTree α β) : Prop

A tree T avoids the target X in the Connes-Kreimer coproduct: T ≠ X and no admissible cut on T extracts X as a subforest element. Equivalently, no summand M ⊗ R of Δ^d T has X ∈ M.

• ne_self : T ≠ X

  T is not literally the target X.

• no_cut (c : CutShape T) : X ∉ c.cutForest

  No admissible cut on T extracts X as a subforest element.

def ConnesKreimer.CutAvoidingForest {α : Type u_1} {β : Type u_2} (F W : TraceForest α β) : Prop

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

Equations

• ConnesKreimer.CutAvoidingForest F W = ∀ T ∈ W, ∀ X ∈ F, ConnesKreimer.CutAvoiding X T

theorem ConnesKreimer.CutAvoidingForest.empty {α : Type u_1} {β : Type u_2} [DecidableEq α] (F : TraceForest α β) : CutAvoidingForest F 0

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

theorem ConnesKreimer.CutAvoidingForest.of_cons {α : Type u_1} {β : Type u_2} [DecidableEq α] {F W : TraceForest α β} {T : TraceTree α β} (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} {β : Type u_2} [DecidableEq α] {F W : TraceForest α β} {T : TraceTree α β} (h : CutAvoidingForest F (T ::ₘ W)) (X : TraceTree α β) : 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} {β : Type u_2} [DecidableEq α] {F W : TraceForest α β} (h : CutAvoidingForest F W) (X : TraceTree α β) : 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} {β : Type u_2} [DecidableEq α] {F W : TraceForest α β} (h : CutAvoidingForest F W) (T : TraceTree α β) : T ∈ W → ∀ X ∈ F, ∀ (c : CutShape T), X ∉ c.cutForest

Workspace-level: no admissible cut on any component T ∈ W extracts any target X ∈ F.

theorem ConnesKreimer.CutAvoidingForest.head_pair {α : Type u_1} {β : Type u_2} [DecidableEq α] {S S' T : TraceTree α β} {W : TraceForest α β} (h : CutAvoidingForest {S, S'} (T ::ₘ W)) : CutAvoiding S T ∧ CutAvoiding S' T

For a workspace T ::ₘ W avoiding the pair-target forest {S, S'}, extract both per-tree avoidances at T. Convenience lemma for the common two-target case (e.g., MCB algebraic Merge with operands S, S').

theorem ConnesKreimer.CutAvoidingForest.not_mem_pair {α : Type u_1} {β : Type u_2} [DecidableEq α] {S S' : TraceTree α β} {W : TraceForest α β} (h : CutAvoidingForest {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-target case.