n-ary trees (generalized Merge)

inductive Minimalism.NaryTree (n : ℕ) : Type

n-ary tree: generalization of SyntacticObject to n-ary branching. When n = 2 this recovers binary trees (= SyntacticObject). When n ≥ 3 this models hypothetical n-ary Merge.

• leaf {n : ℕ} : NaryTree n
• node {n : ℕ} : (Fin n → NaryTree n) → NaryTree n

def Minimalism.NaryTree.leafCount {n : ℕ} : NaryTree n → ℕ

Leaf count of an n-ary tree

Equations

• Minimalism.NaryTree.leaf.leafCount = 1
• (Minimalism.NaryTree.node children).leafCount = ∑ i : Fin n, (children i).leafCount

Achievable leaf counts (Lemma 4.4)

For n-ary trees:

• Binary (n=2): every k ≥ 1 is achievable
• n-ary (n≥3): only k ≡ 1 (mod n-1) are achievable, i.e. k = j(n-1) + 1

def Minimalism.achievableLeafCounts (n : ℕ) : Set ℕ

The set of leaf counts achievable by n-ary trees

Equations

• Minimalism.achievableLeafCounts n = {k : ℕ | ∃ (t : Minimalism.NaryTree n), t.leafCount = k}

theorem Minimalism.leaf_achieves_one (n : ℕ) : 1 ∈ achievableLeafCounts n

A single leaf achieves count 1 for any arity

theorem Minimalism.binary_achieves_two : 2 ∈ achievableLeafCounts 2

Binary trees achieve leaf count 2 (a single node with two leaves)

def Minimalism.NaryTree.expandLeaf : NaryTree 2 → NaryTree 2

Replace the leftmost leaf of a binary tree with a node of two leaves. This increases leafCount by exactly 1.

Equations

• One or more equations did not get rendered due to their size.
• Minimalism.NaryTree.leaf.expandLeaf = Minimalism.NaryTree.node fun (x : Fin 2) => Minimalism.NaryTree.leaf

theorem Minimalism.NaryTree.expandLeaf_leafCount (t : NaryTree 2) : t.expandLeaf.leafCount = t.leafCount + 1

theorem Minimalism.binary_achieves_all (k : ℕ) (hk : k ≥ 1) : k ∈ achievableLeafCounts 2

Binary trees achieve all leaf counts k ≥ 1.

Proof: induction on k. Base k=1: single leaf. Step: expand a leaf to get one more, via expandLeaf which increases leafCount by exactly 1.

def Minimalism.NaryTree.nodeCount {n : ℕ} : NaryTree n → ℕ

Node count of an n-ary tree

Equations

• Minimalism.NaryTree.leaf.nodeCount = 0
• (Minimalism.NaryTree.node children).nodeCount = 1 + ∑ i : Fin n, (children i).nodeCount

theorem Minimalism.nary_leaf_node_relation {n : ℕ} (hn : n ≥ 2) (t : NaryTree n) : t.leafCount = t.nodeCount * (n - 1) + 1

For n-ary trees, leafCount = nodeCount * (n-1) + 1. This is the key structural invariant that implies the modular constraint.

theorem Minimalism.nary_leaf_count_mod {n : ℕ} (hn : n ≥ 2) (t : NaryTree n) : (t.leafCount - 1) % (n - 1) = 0

For n-ary trees (n ≥ 2), leaf count k must satisfy k ≡ 1 (mod n-1).

Each n-ary node replaces 1 "slot" with n children, net gain of n-1 leaves. Starting from 1 leaf, after j nodes we have j(n-1) + 1 leaves.

theorem Minimalism.nary_misses_two (n : ℕ) (hn : n ≥ 3) : 2 ∉ achievableLeafCounts n

For n ≥ 3, not all leaf counts are achievable. Specifically, 2 is not achievable when n ≥ 3 (since 2-1 = 1 is not divisible by n-1 ≥ 2).

theorem Minimalism.binary_unique_optimal (n : ℕ) (hn : n ≥ 2) (h : ∀ k ≥ 1, k ∈ achievableLeafCounts n) : n = 2

Binary Merge is uniquely optimal: it's the only n ≥ 2 that achieves all leaf counts (Lemma 4.4).

Catalan bridge

The number of binary tree shapes with n internal nodes equals the nth Catalan number. We connect this to SyntacticObject via the FreeMagma equivalence.

@[reducible, inline]

abbrev Minimalism.SOShape : Type

Binary tree shape: SO with Unit tokens (only tree structure matters)

Equations

• Minimalism.SOShape = FreeMagma Unit

def Minimalism.freemagmaNodeCount {α : Type u_1} : FreeMagma α → ℕ

Count internal nodes of a FreeMagma tree

Equations

• Minimalism.freemagmaNodeCount (FreeMagma.of a) = 0
• Minimalism.freemagmaNodeCount (a.mul b) = 1 + Minimalism.freemagmaNodeCount a + Minimalism.freemagmaNodeCount b

theorem Minimalism.nodeCount_preserved (so : SyntacticObject) : so.nodeCount = freemagmaNodeCount (toFreeMagma so)

The nodeCount of an SO equals the nodeCount of its FreeMagma image

theorem Minimalism.freemagmaNodeCount_eq_length_sub {α : Type u_1} (fm : FreeMagma α) : freemagmaNodeCount fm = fm.length - 1

Internal node count = FreeMagma.length - 1 for FreeMagma trees

theorem Minimalism.nodeCount_eq_freeMagma_length_sub (so : SyntacticObject) : so.nodeCount = (toFreeMagma so).length - 1

SO.nodeCount = FreeMagma.length - 1 via the isomorphism. Bridges leaf_node_relation to FreeMagma.length.

def Minimalism.SyntacticObject.toShape (so : SyntacticObject) : SOShape

Map an SO to its shape (forget token identity, keep tree structure)

Equations

• so.toShape = (FreeMagma.map fun (x : Minimalism.LIToken) => ()) (Minimalism.toFreeMagma so)

theorem Minimalism.tree_shapes_catalan (n : ℕ) : (Tree.treesOfNumNodesEq n).card = catalan n

The number of binary tree shapes with n internal nodes equals the nth Catalan number.

This is a direct application of mathlib's treesOfNumNodesEq_card_eq_catalan, which counts Tree Unit shapes. The connection to SyntacticObject goes through the FreeMagma ≃ SO equivalence and the well-known bijection between full binary trees and Tree Unit.