Admissible cuts on n-ary rooted trees

[MCB25] [foissy-introduction-hopf-algebras-trees]

An admissible cut of a tree T is a subset of edges such that every root-to-leaf path of T contains at most one selected edge. After deleting the selected edges, T decomposes into:

• The cut forest cutForest c: the multiset of subtrees that get separated from the root after the deletion.
• The remainder: the connected component containing the root, which comes in two flavors:
  • remainderDeletion ≈ MCB's T/^p (admissible cut, Definition 1.2.6, book p. 31): just remove the cut subtrees; the parent vertex now has fewer children, so the remainder lives in the at-most-n-ary substrate (Lemma 1.2.11, book p. 38). NOT MCB's T/^d (Definition 1.2.5), which would re-binarize via edge contraction.
  • remainderTrace ≈ MCB's T/^c (contraction, Definition 1.2.4, book p. 30; requires [Inhabited α]): replace each cut subtree with a single trace-leaf labeled default; the parent's arity is preserved. Used at the C-I (semantic) interface for FormCopy.

This file provides admissible cuts on the n-ary rooted-tree carrier RoseTree α (RoseTree/Basic.lean). The cuts work uniformly across arities — the binary case inherits as a subtype.

Status

[UPSTREAM] candidate. No sorries.

MCB anchor

[MCB25] Definition 1.2.6 (book p. 31) for the admissible cut definition; Lemma 1.2.7 (book p. 32) for the equivalence with forest extraction. Definitions 1.2.4 (T/^c, p. 30), 1.2.5 (T/^d, p. 31), 1.2.6 (T/^p, p. 31) for the three remainder flavors. We expose remainderDeletion (T/^p, p. 31) and remainderTrace (T/^c, p. 30); MCB's T/^d (deletion-then-rebinarize) is not directly exposed here since it's the closest to the consumer- visible "Externalization" form (PF interface) and can be derived from T/^p via tree-binarization at the algebra layer.

§1: The Cut inductive

A cut is recursively built from a per-vertex choice: at the root, for each child edge, decide whether to (a) cut this edge (extracting that subtree), or (b) recurse into that subtree's own cut. The "antichain" condition (no two cuts on the same root-to-leaf path) is baked in because once you cut an edge, you don't recurse beneath it.

inductive RoseTree.Cut {α : Type u_1} : RoseTree α → Type u_1

An admissible cut on a tree T: at the root vertex, a per-child cut decision for each child. (For a leaf, the empty list of children gives the unique trivial cut.)

• mk {α : Type u_1} {a : α} {cs : List (RoseTree α)} (decisions : ChildCutList cs) : (node a cs).Cut

  A cut on a tree, given as a per-child decision list (matching the children list of the root by length).

inductive RoseTree.ChildCut {α : Type u_1} : RoseTree α → Type u_1

A per-child cut decision: either extract (cut the edge and extract this subtree whole) or recurse cut (keep this edge, apply cut to the subtree).

• extract {α : Type u_1} (t : RoseTree α) : t.ChildCut

  Extract this subtree whole.

• recurse {α : Type u_1} {t : RoseTree α} (c : t.Cut) : t.ChildCut

  Don't cut at this edge; recurse into the subtree.

inductive RoseTree.ChildCutList {α : Type u_1} : List (RoseTree α) → Type u_1

A list of ChildCut decisions, indexed by the children list.

• nil {α : Type u_1} : ChildCutList []
• cons {α : Type u_1} {t : RoseTree α} {ts : List (RoseTree α)} (d : t.ChildCut) (ds : ChildCutList ts) : ChildCutList (t :: ts)

§2: The empty cut

For every tree, there is a canonical "empty cut" that recurses everywhere and extracts nothing.

def RoseTree.emptyCut {α : Type u_1} (t : RoseTree α) : t.Cut

The empty cut on a tree: recurse into every child with the empty cut, never extract.

Equations

• (RoseTree.node value cs).emptyCut = RoseTree.Cut.mk (RoseTree.emptyCutList cs)

def RoseTree.emptyCutList {α : Type u_1} (cs : List (RoseTree α)) : ChildCutList cs

The all-recurse decision list for a list of children.

Equations

• RoseTree.emptyCutList [] = RoseTree.ChildCutList.nil
• RoseTree.emptyCutList (t :: ts) = RoseTree.ChildCutList.cons (RoseTree.ChildCut.recurse t.emptyCut) (RoseTree.emptyCutList ts)

def RoseTree.shallowTotalCut {α : Type u_1} (t : RoseTree α) : t.Cut

The total cut: extract every child whole at the root level. (Note: this is shallow — it doesn't recurse. The "total cut" in Foissy's sense extracting the whole tree as a single piece is not directly representable in this Cut type; it lives at the bialgebra layer via the explicit T ⊗ 1 term.)

Equations

• (RoseTree.node value cs).shallowTotalCut = RoseTree.Cut.mk (RoseTree.shallowTotalCut.go cs)

def RoseTree.shallowTotalCut.go {α : Type u_1} (cs : List (RoseTree α)) : ChildCutList cs

Equations

• RoseTree.shallowTotalCut.go [] = RoseTree.ChildCutList.nil
• RoseTree.shallowTotalCut.go (t :: ts) = RoseTree.ChildCutList.cons (RoseTree.ChildCut.extract t) (RoseTree.shallowTotalCut.go ts)

§3: The cut forest

For a cut c : Cut T, cutForest c is the multiset of subtrees extracted by c. We use List for now (the multiset structure emerges at the Hopf algebra layer via Multiset.ofList).

def RoseTree.cutForest {α : Type u_1} {t : RoseTree α} : t.Cut → List (RoseTree α)

The list of subtrees extracted by a cut.

Equations

• RoseTree.cutForest (RoseTree.Cut.mk decisions) = RoseTree.cutForestList decisions

def RoseTree.cutForestList {α : Type u_1} {cs : List (RoseTree α)} : ChildCutList cs → List (RoseTree α)

Auxiliary: extracted subtrees from a child-decision list.

Equations

• RoseTree.cutForestList RoseTree.ChildCutList.nil = []
• RoseTree.cutForestList (RoseTree.ChildCutList.cons d ds) = RoseTree.cutForestChild d ++ RoseTree.cutForestList ds

def RoseTree.cutForestChild {α : Type u_1} {t : RoseTree α} : t.ChildCut → List (RoseTree α)

Auxiliary: extracted subtrees from a single child-decision.

Equations

• RoseTree.cutForestChild (RoseTree.ChildCut.extract x✝) = [x✝]
• RoseTree.cutForestChild (RoseTree.ChildCut.recurse c) = RoseTree.cutForest c

§4: Remainders

Two remainder flavors per MCB §1.11.6:

• remainderDeletion c (T/^p): subtree replaced by nothing (parent loses a child). Arity of remainder vertices may decrease.
• remainderTrace c (T/^c, with [Inhabited α]): subtree replaced by a trace-leaf labeled default. Arity is preserved everywhere.

def RoseTree.remainderDeletion {α : Type u_1} {t : RoseTree α} : t.Cut → RoseTree α

Deletion remainder T/^p: cut subtrees disappear; parent loses children.

Equations

• RoseTree.remainderDeletion (RoseTree.Cut.mk decisions) = RoseTree.node a (RoseTree.remainderDeletionList decisions)

def RoseTree.remainderDeletionList {α : Type u_1} {cs : List (RoseTree α)} : ChildCutList cs → List (RoseTree α)

Auxiliary: deletion remainder for a child-decision list — extracted children disappear from the list.

Equations

• RoseTree.remainderDeletionList RoseTree.ChildCutList.nil = []
• RoseTree.remainderDeletionList (RoseTree.ChildCutList.cons (RoseTree.ChildCut.extract t) ds) = RoseTree.remainderDeletionList ds
• RoseTree.remainderDeletionList (RoseTree.ChildCutList.cons (RoseTree.ChildCut.recurse c) ds) = RoseTree.remainderDeletion c :: RoseTree.remainderDeletionList ds

def RoseTree.remainderTrace {α : Type u_1} [Inhabited α] {t : RoseTree α} : t.Cut → RoseTree α

Trace remainder T/^c: cut subtrees replaced with default-leaves. Arity of all vertices preserved.

Equations

• RoseTree.remainderTrace (RoseTree.Cut.mk decisions) = RoseTree.node a (RoseTree.remainderTraceList decisions)

def RoseTree.remainderTraceList {α : Type u_1} [Inhabited α] {cs : List (RoseTree α)} : ChildCutList cs → List (RoseTree α)

Auxiliary: trace remainder for a child-decision list.

Equations

• RoseTree.remainderTraceList RoseTree.ChildCutList.nil = []
• RoseTree.remainderTraceList (RoseTree.ChildCutList.cons (RoseTree.ChildCut.extract t) ds) = RoseTree.leaf default :: RoseTree.remainderTraceList ds
• RoseTree.remainderTraceList (RoseTree.ChildCutList.cons (RoseTree.ChildCut.recurse c) ds) = RoseTree.remainderTrace c :: RoseTree.remainderTraceList ds

§5: Sanity tests

Verify on a small concrete cut that cutForest, remainderDeletion, and remainderTrace behave as expected.