Branching: the rose-tree interface

A carrier T is Branching when each value exposes an ordered list of children. One field derives, for every instance:

• Gorn-address machinery: subtreeAt, validPaths, daughters
• the dominance order on positions (toTreeOrder), unlocking the [BP90] command-relation library (Core/Order/Command.lean)
• via Core/Order/TreePath.lean, mathlib's rooted-tree order stack on positions: root (⊥), parent (Order.pred), least common ancestor (⊓), finite ancestor chains.

Sibling order (the List) is the load-bearing choice: linear precedence and planarity are real structure that mathlib's Quiver/Digraph/SimpleGraph forget, so those are forgetful shadows of this class, not its basis.

No well-foundedness is required for the base class. The path machinery recurses on the path (structurally decreasing List Nat), not on T, so Branching is law-free on the carrier and still theorem-rich; carriers with infinite depth are admissible. Recursion on the carrier (size, subtrees, yield, inductionOn) needs the IsFiniteBranching mixin below, a Prop-valued well-foundedness assertion on the child relation (mathlib idiom: structure-bearing class + Is… Prop mixin, like RootedTree + IsPredArchimedean).

Known instance candidates across the library (2026-06-06 audit): Syntax.Tree (constituency), NanoTree (Nanosyntax features), CFGTree (CFG derivations — subtreeAt is classical Gorn addressing), RoseTree (Hopf-algebra trees), FreeMagma (bare phrase structure), Dependency-Grammar positions.

class Core.Order.Branching (T : Type u_1) : Type u_1

Rose-tree interface: a carrier with an ordered list of children. [] for leaves. See the module docstring for what one field buys.

• children : T → List T

  Ordered children.

def Core.Order.Branching.IsChild {T : Type u_1} [Branching T] (c t : T) : Prop

The "is a child of" relation on a Branching carrier.

Equations

• Core.Order.Branching.IsChild c t = (c ∈ Core.Order.Branching.children t)

@[reducible, inline]

abbrev Core.Order.Branching.daughters {T : Type u_1} [Branching T] (t : T) : List T

Daughters of a node — children, by its linguistic name.

Equations

• Core.Order.Branching.daughters t = Core.Order.Branching.children t

def Core.Order.Branching.subtreeAt {T : Type u_1} [Branching T] (t : T) : List ℕ → Option T

Subtree at a Gorn address; none if the path leaves the tree. Recursion is on the path, so no well-foundedness on T is needed.

Equations

• Core.Order.Branching.subtreeAt t [] = some t
• Core.Order.Branching.subtreeAt t (i :: rest) = (Core.Order.Branching.children t)[i]?.bind fun (c : T) => Core.Order.Branching.subtreeAt c rest

@[simp]

theorem Core.Order.Branching.subtreeAt_nil {T : Type u_1} [Branching T] (t : T) : subtreeAt t [] = some t

@[simp]

theorem Core.Order.Branching.subtreeAt_cons {T : Type u_1} [Branching T] (t : T) (i : ℕ) (rest : List ℕ) : subtreeAt t (i :: rest) = (children t)[i]?.bind fun (c : T) => subtreeAt c rest

def Core.Order.Branching.validPaths {T : Type u_1} [Branching T] (t : T) : Set TreePath

Valid positions of a tree. Node identity is the position (TreePath), never the subtree value: identical subtrees occur at multiple positions, so orders and graphs must live on paths.

Equations

• Core.Order.Branching.validPaths t = {p : Core.Order.TreePath | (Core.Order.Branching.subtreeAt t p.toList).isSome = true}

theorem Core.Order.Branching.bot_mem_validPaths {T : Type u_1} [Branching T] (t : T) : ⊥ ∈ validPaths t

theorem Core.Order.Branching.subtreeAt_append {T : Type u_1} [Branching T] (t : T) (p q : List ℕ) : subtreeAt t (p ++ q) = (subtreeAt t p).bind fun (x : T) => subtreeAt x q

Gorn-address composition: descending along p ++ q is descending along p, then along q from there.

theorem Core.Order.Branching.mem_validPaths_cons {T : Type u_1} [Branching T] {t : T} {i : ℕ} {rest : List ℕ} : { toList := i :: rest } ∈ validPaths t ↔ ∃ (c : T), (children t)[i]? = some c ∧ { toList := rest } ∈ validPaths c

Membership characterization for non-root positions: descend one child, then recurse.

theorem Core.Order.Branching.validPaths_prefix_closed {T : Type u_1} [Branching T] {t : T} {p q : TreePath} (hq : q ∈ validPaths t) (hpq : p ≤ q) : p ∈ validPaths t

Valid paths are closed under prefixes (ancestors of a position are positions): the set of positions is downward closed, hence inherits the rooted-tree order stack from TreePath.

def Core.Order.Branching.toTreeOrder {T : Type u_1} [Branching T] (t : T) : TreeOrder TreePath

The dominance order of any Branching carrier, as a [BP90] TreeOrder on positions. Every instance inherits the command-relation library through this single definition — generalizing the former Syntax.Tree.toTreeOrder.

Equations

• Core.Order.Branching.toTreeOrder t = { nodes := Core.Order.Branching.validPaths t, root := ⊥, root_in_nodes := ⋯, root_le_all := ⋯, ancestor_connected := ⋯ }

IsFiniteBranching: the well-foundedness mixin

Prop-valued mixin asserting that Branching.IsChild is well-founded on T — i.e. every descent chain is finite. Unlocks carrier recursion (size, subtrees, yield, inductionOn) via WellFounded.fix.

Mathlib idiom: structure-bearing class (Branching) + Is… Prop mixin asserting a property (IsFiniteBranching), like PartialOrder

• IsPredArchimedean in RootedTree. The mixin is Prop so instances are never noncomputable; concrete inductives discharge it via Subrelation.wf against the auto-derived sizeOf well-founded relation (one-liner per instance). Carriers without auto-SizeOf (e.g. FreeMagma, whose genSizeOfSpec is false) discharge via Acc.intro + the carrier's recursor.

Previously this was a data class carrying measure : T → Nat, but that design forced noncomputable on inductive instances (LCNF crash on nested-List recursors) and broke equation-theorem elaboration for downstream WF defs. The redesign — Prop mixin + compile_inductive% at inductive definition sites — fixes both.

class Core.Order.IsFiniteBranching (T : Type u_1) [Branching T] : Prop

A Branching carrier whose "is a child of" relation is well-founded — i.e. every descent chain ends. Unlocks carrier recursion.

• wf : WellFounded Branching.IsChild

theorem Core.Order.IsFiniteBranching.ofMeasure {T : Type u_1} [Branching T] (m : T → ℕ) (h : ∀ {c t : T}, c ∈ Branching.children t → m c < m t) : IsFiniteBranching T

Build IsFiniteBranching T from any Nat-valued measure that children strictly decrease (canonically sizeOf for inductives).

def Core.Order.Branching.size {T : Type u_1} [Branching T] [IsFiniteBranching T] (t : T) : ℕ

Number of nodes.

Equations

• One or more equations did not get rendered due to their size.

theorem Core.Order.Branching.size_eq {T : Type u_1} [Branching T] [IsFiniteBranching T] (t : T) : size t = 1 + (List.map (fun (x : { x : T // x ∈ children t }) => match x with | ⟨c, property⟩ => size c) (children t).attach).sum

One-step unfolding of size. Proved by WellFounded.fix_eq.

theorem Core.Order.Branching.size_def {T : Type u_1} [Branching T] [IsFiniteBranching T] (t : T) : size t = 1 + (List.map size (children t)).sum

Attach-free unfolding of size, for concrete computation.

def Core.Order.Branching.subtrees {T : Type u_1} [Branching T] [IsFiniteBranching T] (t : T) : List T

All subtrees including self, pre-order.

Equations

• One or more equations did not get rendered due to their size.

theorem Core.Order.Branching.subtrees_eq {T : Type u_1} [Branching T] [IsFiniteBranching T] (t : T) : subtrees t = t :: List.flatMap (fun (x : { x : T // x ∈ children t }) => match x with | ⟨c, property⟩ => subtrees c) (children t).attach

theorem Core.Order.Branching.subtrees_def {T : Type u_1} [Branching T] [IsFiniteBranching T] (t : T) : subtrees t = t :: List.flatMap subtrees (children t)

Attach-free unfolding of subtrees, for concrete computation.

theorem Core.Order.Branching.self_mem_subtrees {T : Type u_1} [Branching T] [IsFiniteBranching T] (t : T) : t ∈ subtrees t

def Core.Order.Branching.inductionOn {T : Type u_1} [Branching T] [IsFiniteBranching T] {motive : T → Sort u_2} (t : T) (ih : (t : T) → ((c : T) → c ∈ children t → motive c) → motive t) : motive t

Strong induction over an IsFiniteBranching carrier: prove motive t from motive on all children. Canonical mathlib pattern — delegates to WellFounded.fix.

Equations

• One or more equations did not get rendered due to their size.

theorem Core.Order.Branching.inductionOn_eq {T : Type u_1} [Branching T] [IsFiniteBranching T] {motive : T → Sort u_2} (t : T) (ih : (t : T) → ((c : T) → c ∈ children t → motive c) → motive t) : inductionOn t ih = ih t fun (c : T) (x : c ∈ children t) => inductionOn c ih

HasContent and yield

Separate class because not every rose-tree carrier has terminal content (Nanosyntax trees carry features on every node; CFG derivation trees distinguish terminal from nonterminal types).

class Core.Order.HasContent (T : Type u_1) (W : outParam (Type u_2)) : Type (max u_1 u_2)

Carriers whose nodes may carry pronounceable terminal content. W is an outParam: in linguistics use each carrier has one content reading. (Multi-content scenarios — phonological vs orthographic — can be supported via different wrapper types if needed.)

• content? : T → Option W

  Terminal content, if any.

def Core.Order.Branching.yield {T : Type u_1} {W : Type u_2} [Branching T] [IsFiniteBranching T] [HasContent T W] (t : T) : List W

Terminal yield, left to right: the frontier string. The most basic tree-to-string map — linear precedence lives over it.

Equations

• One or more equations did not get rendered due to their size.

theorem Core.Order.Branching.yield_eq {T : Type u_1} {W : Type u_2} [Branching T] [IsFiniteBranching T] [HasContent T W] (t : T) : yield t = (content? t).toList ++ List.flatMap (fun (x : { x : T // x ∈ children t }) => match x with | ⟨c, property⟩ => yield c) (children t).attach

theorem Core.Order.Branching.yield_def {T : Type u_1} {W : Type u_2} [Branching T] [IsFiniteBranching T] [HasContent T W] (t : T) : yield t = (content? t).toList ++ List.flatMap yield (children t)

Attach-free unfolding of yield, for concrete computation.

Yield with positions — the precedence-is-yield-order substrate

yieldWithPaths pairs each terminal with its Gorn address. Defined via WellFounded.fix (not Lean's WF elaborator) so its unfold lemma is a one-liner via WellFounded.fix_eq — the mathlib-reviewer's escape from the equation-compiler timeout that the earlier attach.zipIdx.flatMap formulation hit. The pairwise-Precedes bridge (Precedes is yield order, [Kay94] LCA-style) is a follow-up that builds on this substrate.

def Core.Order.Branching.yieldWithPaths {T : Type u_1} {W : Type u_2} [Branching T] [IsFiniteBranching T] [HasContent T W] (t : T) : List (TreePath × W)

Yield with positions: each terminal paired with its Gorn address.

Equations

• One or more equations did not get rendered due to their size.

theorem Core.Order.Branching.yieldWithPaths_eq {T : Type u_1} {W : Type u_2} [Branching T] [IsFiniteBranching T] [HasContent T W] (t : T) : yieldWithPaths t = List.map (fun (x : W) => (⊥, x)) (content? t).toList ++ List.flatMap (fun (ci : { x : T // x ∈ children t } × ℕ) => List.map (fun (pw : TreePath × W) => ({ toList := ci.2 :: pw.1.toList }, pw.2)) (yieldWithPaths ↑ci.1)) (children t).attach.zipIdx

One-step unfolding of yieldWithPaths, by WellFounded.fix_eq — the lemma that the old WF-elaborator approach could not produce.

Instance: FreeMagma

Mathlib's free magma is the binary rose tree (bare phrase structure in the Minimalist reading); the instance lives here because mathlib types take their instances in the class's home file. FreeMagma is declared with set_option genSizeOfSpec false, so IsFiniteBranching cannot use the sizeOf shortcut — but the inductive recursor FreeMagma.recOnMul suffices for a direct Acc.intro proof.

@[implicit_reducible]

instance Core.Order.instBranchingFreeMagma {α : Type u_1} : Branching (FreeMagma α)

Equations

• Core.Order.instBranchingFreeMagma = { children := fun (x : FreeMagma α) => match x with | FreeMagma.of a => [] | l.mul r => [l, r] }

@[simp]

theorem Core.Order.freeMagma_children_of {α : Type u_1} (a : α) : Branching.children (FreeMagma.of a) = []

@[simp]

theorem Core.Order.freeMagma_children_mul {α : Type u_1} (l r : FreeMagma α) : Branching.children (l.mul r) = [l, r]

instance Core.Order.instIsFiniteBranchingFreeMagma {α : Type u_1} : IsFiniteBranching (FreeMagma α)

Decidable command relations over toTreeOrder

commandRelation (toTreeOrder t) P is decidable at concrete positions: the dominators of a are exactly the prefixes of a's path (List.inits), a finite list, so the defining universal collapses to a List-bounded one. This unlocks decide for c-command facts on concrete trees ([BP90], [Rei76]). The branching property is supplied by isBranchingAt (≥ 2 children at the position), the geometric reading of [Rei76]'s "branching node".

@[implicit_reducible]

instance Core.Order.Branching.instDecidableLETreePath : DecidableLE TreePath

Dominance (p ≤ q, prefix order) on positions is decidable.

Equations

• Core.Order.Branching.instDecidableLETreePath p q = decidable_of_iff (p.toList <+: q.toList) ⋯

def Core.Order.Branching.isBranchingAt {T : Type u_1} [Branching T] (t : T) (p : TreePath) : Prop

A position p is a branching node of t when its subtree has at least two children — the geometric reading of [Rei76]'s "first branching node" generating relation.

Equations

• Core.Order.Branching.isBranchingAt t p = ∃ (s : T), Core.Order.Branching.subtreeAt t p.toList = some s ∧ 2 ≤ (Core.Order.Branching.children s).length

@[implicit_reducible]

instance Core.Order.Branching.decIsBranchingAt {T : Type u_1} [Branching T] (t : T) (p : TreePath) : Decidable (isBranchingAt t p)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Core.Order.Branching.instDecidablePredTreePathIsBranchingAt {T : Type u_1} [Branching T] (t : T) : DecidablePred (isBranchingAt t)

Equations

• Core.Order.Branching.instDecidablePredTreePathIsBranchingAt t p = Core.Order.Branching.decIsBranchingAt t p

theorem Core.Order.Branching.mem_commandRelation_toTreeOrder_iff {T : Type u_1} [Branching T] (t : T) (P : Set TreePath) (a b : TreePath) : (a, b) ∈ commandRelation (toTreeOrder t) P ↔ ∀ x ∈ List.map TreePath.mk a.toList.inits, x ≠ a → x ∈ P → x ≤ b

Membership in commandRelation (toTreeOrder t) P collapses to a finite universal over the proper prefixes of a: the only nodes that properly dominate a are its proper prefixes (a.toList.inits). This is the key reduction making c-command facts decide-able.

@[implicit_reducible]

instance Core.Order.Branching.decMemCommandRelation {T : Type u_1} [Branching T] (t : T) (P : Set TreePath) [DecidablePred fun (x : TreePath) => x ∈ P] (a b : TreePath) : Decidable ((a, b) ∈ commandRelation (toTreeOrder t) P)

Equations

• Core.Order.Branching.decMemCommandRelation t P a b = decidable_of_iff (∀ x ∈ List.map Core.Order.TreePath.mk a.toList.inits, x ≠ a → x ∈ P → x ≤ b) ⋯

@[reducible, inline]

abbrev Core.Order.Branching.cCommandAt {T : Type u_1} [Branching T] (t : T) : Set (TreePath × TreePath)

c-command over a concrete carrier ([Rei76]'s c-command): the [BP90] command relation generated by the geometric branching nodes isBranchingAt t. Unlike the abstract cCommand (Core/Order/Command.lean, parameterised by the order-theoretic branchingNodes), this reads the branching property directly off the carrier, so it is decidable and matches sister-form c-command on binary trees. abbrev so membership inherits decMemCommandRelation.

Equations

• Core.Order.Branching.cCommandAt t = Core.Order.commandRelation (Core.Order.Branching.toTreeOrder t) {p : Core.Order.TreePath | Core.Order.Branching.isBranchingAt t p}

Computability sentinels

Branching.size/yield on FreeMagma reduce by decide at concrete data — protecting against noncomputable-regressions during refactors.