Admissible cuts on planar n-ary rooted trees #

@cite{marcolli-chomsky-berwick-2025} @cite{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 RootedTree.Planar α (the list-based n-ary planar carrier from Planar.lean). The cuts work uniformly across arities — the binary case inherits as a subtype.

Status #

[UPSTREAM] candidate. No sorries.

MCB anchor #

@cite{marcolli-chomsky-berwick-2025} 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.

source

inductive RootedTree.Planar.Cut {α : Type u_1} :

Planar α → 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 (Planar α)} (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).

Instances For

source

inductive RootedTree.Planar.ChildCut {α : Type u_1} :

Planar α → 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 : Planar α) : t.ChildCut
Extract this subtree whole.
recurse {α : Type u_1} {t : Planar α} (c : t.Cut) : t.ChildCut
Don't cut at this edge; recurse into the subtree.

Instances For

source

inductive RootedTree.Planar.ChildCutList {α : Type u_1} :

List (Planar α) → Type u_1

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

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

Instances For

§2: The empty cut #

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

source

def RootedTree.Planar.emptyCut {α : Type u_1} (t : Planar α) :

t.Cut

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

Equations

(RootedTree.Planar.node a cs).emptyCut = RootedTree.Planar.Cut.mk (RootedTree.Planar.emptyCutList cs)

Instances For

source

def RootedTree.Planar.emptyCutList {α : Type u_1} (cs : List (Planar α)) :

ChildCutList cs

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

Equations

Instances For

source

def RootedTree.Planar.shallowTotalCut {α : Type u_1} (t : Planar α) :

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

(RootedTree.Planar.node a cs).shallowTotalCut = RootedTree.Planar.Cut.mk (RootedTree.Planar.shallowTotalCut.go cs)

Instances For

source

def RootedTree.Planar.shallowTotalCut.go {α : Type u_1} (cs : List (Planar α)) :

ChildCutList cs

Equations

Instances For

§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).

source

def RootedTree.Planar.cutForest {α : Type u_1} {t : Planar α} :

t.Cut → List (Planar α)

The list of subtrees extracted by a cut.

Equations

RootedTree.Planar.cutForest (RootedTree.Planar.Cut.mk decisions) = RootedTree.Planar.cutForestList decisions

Instances For

source

def RootedTree.Planar.cutForestList {α : Type u_1} {cs : List (Planar α)} :

ChildCutList cs → List (Planar α)

Auxiliary: extracted subtrees from a child-decision list.

Equations

Instances For

source

def RootedTree.Planar.cutForestChild {α : Type u_1} {t : Planar α} :

t.ChildCut → List (Planar α)

Auxiliary: extracted subtrees from a single child-decision.

Equations

Instances For

§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.

source