Leaves, rank, decision lists, and energy of decision trees

The Boolean answers along a root-to-leaf path identify the reached leaf, even when different leaves have the same label. The structural leaf count includes unreachable leaves and exceeds the internal node count by one. A tree of depth d has at most 2 ^ d leaves; refined by Ehrenfeucht–Haussler rank r or by right-branch energy e, it has at most ∑ j ∈ Finset.range (r + 1), d.choose j or ∑ j ∈ Finset.range (e + 1), d.choose j leaves. Decision lists have rank at most 1, hence at most d + 1 leaves and d internal nodes.

The energy bound is attained by ordered threshold comparisons: every positive number of leaves up to BitString.ballSize q e is realized at depth at most q and energy at most e. The construction returns each consecutive input index at its own leaf, so none of the counted leaves is unreachable. This is the ordered-tree step of the scalar capacity theorem, not a construction of native weighted-threshold circuits.

Main definitions

• Cslib.DecisionTree.leafCount: the number of structural leaves.
• Cslib.DecisionTree.nodeCount: the number of internal query nodes.
• Cslib.DecisionTree.path: the answers along the path taken by an input.
• Cslib.DecisionTree.rank: the Ehrenfeucht–Haussler rank of a binary decision tree.
• Cslib.DecisionTree.IsDecisionList: trees in which every internal node has a leaf child.
• Cslib.DecisionTree.energy: the maximum number of true branches on a root-to-leaf path.

Main results

• Cslib.DecisionTree.eval_eq_of_path_eq: a common path gives a common output.
• Cslib.DecisionTree.leafCount_eq_nodeCount_add_one: a binary tree has one more leaf than internal nodes.
• Cslib.DecisionTree.leafCount_le_two_pow_depth: a tree of depth d has at most 2 ^ d leaves.
• Cslib.DecisionTree.leafCount_le_sum_choose_rank: a tree of depth d and rank r has at most ∑ j ≤ r, d.choose j leaves.
• Cslib.DecisionTree.IsDecisionList.rank_le_one: every decision list has rank at most 1.
• Cslib.DecisionTree.leafCount_le_sum_choose_energy: a tree of depth d and energy e has at most ∑ j ≤ e, d.choose j leaves.
• Cslib.DecisionTree.exists_orderedComparisonTree_iff: the exact leaf capacity of ordered comparison trees, with an evaluation specification for every consecutive input index.

References

• Threshold Circuits as Decision Trees and Finite-State Programs, Section 2.2 and the ordered-tree construction in the proof of Theorem 4.1

def Cslib.DecisionTree.leafCount {ι : Type u_1} {β : Type u_2} : DecisionTree ι β → ℕ

The number of structural leaves, including any unreachable leaves.

def Cslib.DecisionTree.path {ι : Type u_1} {β : Type u_2} : DecisionTree ι β → (ι → Bool) → List Bool

The answers along the path to the reached leaf.

theorem Cslib.DecisionTree.leafCount_pos {ι : Type u_1} {β : Type u_2} (t : DecisionTree ι β) : 0 < t.leafCount

Every decision tree has at least one structural leaf.

theorem Cslib.DecisionTree.leafCount_le_two_pow_depth {ι : Type u_1} {β : Type u_2} (t : DecisionTree ι β) : t.leafCount ≤ 2 ^ t.depth

A decision tree of depth d has at most 2 ^ d structural leaves.

theorem Cslib.DecisionTree.eval_eq_of_path_eq {ι : Type u_1} {β : Type u_2} (t : DecisionTree ι β) {x y : ι → Bool} (h : t.path x = t.path y) : t.eval x = t.eval y

Inputs following the same path reach the same leaf label.

@[simp]

theorem Cslib.DecisionTree.leafCount_mapQueries {ι : Type u_1} {β : Type u_2} {κ : Type u_3} (f : ι → κ) (t : DecisionTree ι β) : (mapQueries f t).leafCount = t.leafCount

Relabelling queries preserves the structural leaf count, including unreachable leaves.

@[simp]

theorem Cslib.DecisionTree.path_mapQueries {ι : Type u_1} {β : Type u_2} {κ : Type u_3} (f : ι → κ) (t : DecisionTree ι β) (x : κ → Bool) : (mapQueries f t).path x = t.path (x ∘ f)

Relabelling queries preserves the path taken by an input.

def Cslib.DecisionTree.nodeCount {ι : Type u_1} {β : Type u_2} : DecisionTree ι β → ℕ

The number of internal query nodes, including any unreachable subtrees.

@[simp]

theorem Cslib.DecisionTree.nodeCount_leaf {ι : Type u_1} {β : Type u_2} (b : β) : (leaf b).nodeCount = 0

@[simp]

theorem Cslib.DecisionTree.nodeCount_node {ι : Type u_1} {β : Type u_2} (i : ι) (left right : DecisionTree ι β) : (node i left right).nodeCount = left.nodeCount + right.nodeCount + 1

theorem Cslib.DecisionTree.leafCount_eq_nodeCount_add_one {ι : Type u_1} {β : Type u_2} (t : DecisionTree ι β) : t.leafCount = t.nodeCount + 1

The structural leaf count exceeds the internal node count by one.

@[simp]

theorem Cslib.DecisionTree.nodeCount_mapQueries {ι : Type u_1} {β : Type u_2} {κ : Type u_3} (f : ι → κ) (t : DecisionTree ι β) : (mapQueries f t).nodeCount = t.nodeCount

Relabelling queries preserves the internal node count.

def Cslib.DecisionTree.rank {ι : Type u_1} {β : Type u_2} : DecisionTree ι β → ℕ

The Ehrenfeucht–Haussler rank of a binary decision tree: leaves have rank zero, a node with unequal child ranks has their maximum, and equal child ranks r give rank r + 1.

@[simp]

theorem Cslib.DecisionTree.rank_leaf {ι : Type u_1} {β : Type u_2} (b : β) : (leaf b).rank = 0

@[simp]

theorem Cslib.DecisionTree.rank_mapQueries {ι : Type u_1} {β : Type u_2} {κ : Type u_3} (f : ι → κ) (t : DecisionTree ι β) : (mapQueries f t).rank = t.rank

Relabelling queries preserves the rank.

theorem Cslib.DecisionTree.rank_le_depth {ι : Type u_1} {β : Type u_2} (t : DecisionTree ι β) : t.rank ≤ t.depth

The rank of a decision tree is at most its depth.

theorem Cslib.DecisionTree.leafCount_le_sum_choose_of_rank_le {ι : Type u_1} {β : Type u_2} (t : DecisionTree ι β) {r d : ℕ} (hr : t.rank ≤ r) (hd : t.depth ≤ d) : t.leafCount ≤ ∑ j ∈ Finset.range (r + 1), d.choose j

A decision tree of rank at most r and depth at most d has at most ∑ j ∈ Finset.range (r + 1), d.choose j structural leaves.

theorem Cslib.DecisionTree.leafCount_le_sum_choose_rank {ι : Type u_1} {β : Type u_2} (t : DecisionTree ι β) : t.leafCount ≤ ∑ j ∈ Finset.range (t.rank + 1), t.depth.choose j

A decision tree of depth d and rank r has at most ∑ j ∈ Finset.range (r + 1), d.choose j structural leaves.

theorem Cslib.DecisionTree.leafCount_le_depth_add_one_of_rank_le_one {ι : Type u_1} {β : Type u_2} (t : DecisionTree ι β) (hr : t.rank ≤ 1) : t.leafCount ≤ t.depth + 1

A decision tree of rank at most 1 has at most depth + 1 structural leaves.

theorem Cslib.DecisionTree.nodeCount_le_depth_of_rank_le_one {ι : Type u_1} {β : Type u_2} (t : DecisionTree ι β) (hr : t.rank ≤ 1) : t.nodeCount ≤ t.depth

A decision tree of rank at most 1 has at most depth internal nodes.

def Cslib.DecisionTree.IsDecisionList {ι : Type u_1} {β : Type u_2} : DecisionTree ι β → Prop

A binary decision tree is a decision list when every internal node has at least one leaf child (leafCount = 1).

theorem Cslib.DecisionTree.rank_eq_zero_of_leafCount_eq_one {ι : Type u_1} {β : Type u_2} {t : DecisionTree ι β} (h : t.leafCount = 1) : t.rank = 0

A tree with a single structural leaf has rank zero.

theorem Cslib.DecisionTree.IsDecisionList.rank_le_one {ι : Type u_1} {β : Type u_2} {t : DecisionTree ι β} (h : t.IsDecisionList) : t.rank ≤ 1

Every decision list has Ehrenfeucht–Haussler rank at most 1.

theorem Cslib.DecisionTree.IsDecisionList.leafCount_le_depth_add_one {ι : Type u_1} {β : Type u_2} {t : DecisionTree ι β} (h : t.IsDecisionList) : t.leafCount ≤ t.depth + 1

A decision list has at most depth + 1 structural leaves.

theorem Cslib.DecisionTree.IsDecisionList.nodeCount_le_depth {ι : Type u_1} {β : Type u_2} {t : DecisionTree ι β} (h : t.IsDecisionList) : t.nodeCount ≤ t.depth

A decision list has at most depth internal nodes.

theorem Cslib.DecisionTree.IsDecisionList.mapQueries {ι : Type u_1} {β : Type u_2} {κ : Type u_3} (f : ι → κ) {t : DecisionTree ι β} (h : t.IsDecisionList) : (DecisionTree.mapQueries f t).IsDecisionList

Relabelling queries preserves decision-list structure.

def Cslib.DecisionTree.energy {ι : Type u_1} {β : Type u_2} : DecisionTree ι β → ℕ

The energy of a binary decision tree: the maximum number of true (right) branches on a root-to-leaf path.

@[simp]

theorem Cslib.DecisionTree.energy_leaf {ι : Type u_1} {β : Type u_2} (b : β) : (leaf b).energy = 0

@[simp]

theorem Cslib.DecisionTree.energy_mapQueries {ι : Type u_1} {β : Type u_2} {κ : Type u_3} (f : ι → κ) (t : DecisionTree ι β) : (mapQueries f t).energy = t.energy

Relabelling queries preserves the energy.

theorem Cslib.DecisionTree.energy_le_depth {ι : Type u_1} {β : Type u_2} (t : DecisionTree ι β) : t.energy ≤ t.depth

The energy of a decision tree is at most its depth.

theorem Cslib.DecisionTree.leafCount_le_sum_choose_of_energy_le {ι : Type u_1} {β : Type u_2} (t : DecisionTree ι β) {e d : ℕ} (he : t.energy ≤ e) (hd : t.depth ≤ d) : t.leafCount ≤ ∑ j ∈ Finset.range (e + 1), d.choose j

A decision tree of energy at most e and depth at most d has at most ∑ j ∈ Finset.range (e + 1), d.choose j structural leaves.

theorem Cslib.DecisionTree.leafCount_le_sum_choose_energy {ι : Type u_1} {β : Type u_2} (t : DecisionTree ι β) : t.leafCount ≤ ∑ j ∈ Finset.range (t.energy + 1), t.depth.choose j

A decision tree of depth d and energy e has at most ∑ j ∈ Finset.range (e + 1), d.choose j structural leaves.

theorem Cslib.DecisionTree.exists_orderedComparisonTree_iff (q e L a : ℕ) : (∃ (t : DecisionTree ℕ ℕ), t.leafCount = L ∧ t.depth ≤ q ∧ t.energy ≤ e ∧ ∀ j < L, (t.eval fun (k : ℕ) => decide (k ≤ a + j)) = a + j) ↔ 0 < L ∧ L ≤ BitString.ballSize q e

Exact ordered query-activity capacity. A tree making scalar threshold comparisons has exactly L leaves, depth at most q, and true-branch energy at most e, with distinct outputs on L consecutive scalar inputs, if and only if 0 < L ≤ BitString.ballSize q e.

Query k asks whether k ≤ a + j; on input a + j, for j < L, the output is a + j. The arbitrary offset a lets the construction recurse on adjacent intervals. The theorem includes zero depth, zero energy, and energy budgets exceeding depth. It formalizes the ordered-tree construction in the proof of Theorem 4.1 of [26], not the subsequent compilation into a native weighted-threshold circuit.