Canonical deepest paths in finite decision trees

Every finite decision tree has a deterministically chosen deepest path whose length is exactly the tree depth. For path-read-once trees, every prefix of that path is an embedding into the input coordinates.

theorem Complexity.DecisionTree.On.pathReadOnce_neg {N : ℕ} (tree : On N) : tree.neg.PathReadOnce ↔ tree.PathReadOnce

Complementing the leaves preserves the path-read-once property.

theorem Complexity.DecisionTree.On.length_deepPath {N : ℕ} (tree : On N) : tree.deepPath.length = tree.depth

The chosen deepest path has length exactly equal to tree depth.

theorem Complexity.DecisionTree.On.mem_vars_of_mem_deepPath {N : ℕ} (tree : On N) (query : Fin N × Bool) (hquery : query ∈ tree.deepPath) : query.1 ∈ tree.vars

Every query on the chosen path occurs in the tree's variable set.

theorem Complexity.DecisionTree.On.nodup_deepPathVars {N : ℕ} (tree : On N) (readOnce : tree.PathReadOnce) : tree.deepPathVars.Nodup

A path-read-once tree has no repeated query on its chosen deepest path.

theorem Complexity.DecisionTree.On.depth_le_card_vars_of_pathReadOnce {N : ℕ} (tree : On N) (readOnce : tree.PathReadOnce) : tree.depth ≤ tree.vars.card

A path-read-once tree has depth at most the number of distinct variables it queries anywhere.