Canonical deepest paths in finite decision trees -- proof internals

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

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

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

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

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

noncomputable def Complexity.DecisionTree.On.deepPrefixEmbeddingInternal {N : ℕ} (tree : On N) (queryCount : ℕ) (hdepth : queryCount ≤ tree.depth) (readOnce : tree.PathReadOnce) : Fin queryCount ↪ Fin N

The first queryCount query indices on a deep path, packaged as an embedding when the whole tree is path-read-once.

Equations

• tree.deepPrefixEmbeddingInternal queryCount hdepth readOnce = { toFun := fun (position : Fin queryCount) => tree.deepPathVars.get (Fin.castLE ⋯ position), inj' := ⋯ }

noncomputable def Complexity.DecisionTree.On.deepPrefixValuesInternal {N : ℕ} (tree : On N) (queryCount : ℕ) (hdepth : queryCount ≤ tree.depth) : Fin queryCount → Bool

Branch bit at each of the first queryCount positions of the chosen deep path.

Equations

• tree.deepPrefixValuesInternal queryCount hdepth position = (tree.deepPath.get (Fin.castLE ⋯ position)).2

theorem Complexity.DecisionTree.On.deepPrefixEmbedding_mem_vars_internal {N : ℕ} (tree : On N) (queryCount : ℕ) (hdepth : queryCount ≤ tree.depth) (readOnce : tree.PathReadOnce) (position : Fin queryCount) : (tree.deepPrefixEmbeddingInternal queryCount hdepth readOnce) position ∈ tree.vars