Finite-arity decision trees

DecisionTree.On N records the input arity in its query labels. It is the decision-tree representation used by finite switching and restriction arguments; no query can silently fall outside the sampled variable set.

theorem Complexity.DecisionTree.On.eval_toDecisionTree {N : ℕ} (input : BitString N) (tree : On N) : DecisionTree.eval input.toTotal tree.toDecisionTree = eval input tree

Erasing query bounds preserves evaluation on the canonical total extension of a bit string.

theorem Complexity.DecisionTree.On.depth_toDecisionTree {N : ℕ} (tree : On N) : tree.toDecisionTree.depth = tree.depth

Erasing query bounds preserves depth exactly.

theorem Complexity.DecisionTree.On.numLeaves_toDecisionTree {N : ℕ} (tree : On N) : tree.toDecisionTree.numLeaves = tree.numLeaves

Erasing query bounds preserves leaf count exactly.

theorem Complexity.DecisionTree.On.numLeaves_le_two_pow_depth {N : ℕ} (tree : On N) : tree.numLeaves ≤ 2 ^ tree.depth

A depth-d finite decision tree has at most 2 ^ d leaves.

theorem Complexity.DecisionTree.On.card_vars_le_arity {N : ℕ} (tree : On N) : tree.vars.card ≤ N

A finite-arity tree queries at most its declared number of variables.

theorem Complexity.DecisionTree.On.eval_neg {N : ℕ} (input : BitString N) (tree : On N) : eval input tree.neg = !eval input tree

Negating every leaf complements the computed function.

theorem Complexity.DecisionTree.On.depth_neg {N : ℕ} (tree : On N) : tree.neg.depth = tree.depth

Leaf negation preserves query depth exactly.

theorem Complexity.DecisionTree.On.numLeaves_neg {N : ℕ} (tree : On N) : tree.neg.numLeaves = tree.numLeaves

Leaf negation preserves the number of leaves exactly.

theorem Complexity.DecisionTree.On.vars_neg {N : ℕ} (tree : On N) : tree.neg.vars = tree.vars

Leaf negation preserves the queried-variable set exactly.

theorem Complexity.DecisionTree.On.eval_restrict {N : ℕ} (restriction : Restriction.On N) (input : BitString N) (tree : On N) : eval input (restrict restriction tree) = eval (restriction.applyTo input) tree

Restriction commutes with finite-tree evaluation.

theorem Complexity.DecisionTree.On.depth_restrict_le {N : ℕ} (restriction : Restriction.On N) (tree : On N) : (restrict restriction tree).depth ≤ tree.depth

Restriction cannot increase finite decision-tree depth.

theorem Complexity.DecisionTree.On.vars_restrict_subset_filter {N : ℕ} (restriction : Restriction.On N) (tree : On N) : (restrict restriction tree).vars ⊆ {index ∈ tree.vars | restriction index = none}

Every query surviving restriction was queried originally and remains free.

@[simp]

theorem Complexity.DecisionTree.On.restrict_empty {N : ℕ} (tree : On N) : restrict Restriction.On.empty tree = tree

theorem Complexity.DecisionTree.On.restrict_comp {N : ℕ} (first second : Restriction.On N) (tree : On N) : restrict second (restrict first tree) = restrict (first.comp second) tree

Sequential restriction agrees with left-biased finite composition.