Complete query blocks in finite decision trees

This module exposes a reusable complete query block: every listed coordinate is queried before control reaches a continuation indexed by the collected finite restriction.

theorem Complexity.DecisionTree.On.assignmentFor_apply_of_mem {N : ℕ} (queries : List (Fin N)) (input : BitString N) (index : Fin N) (hmem : index ∈ queries) : assignmentFor queries input index = some (input index)

Every listed coordinate is fixed to the value read from the input.

theorem Complexity.DecisionTree.On.assignmentFor_apply_of_not_mem {N : ℕ} (queries : List (Fin N)) (input : BitString N) (index : Fin N) (hmem : index ∉ queries) : assignmentFor queries input index = none

Every coordinate outside the query list remains free.

theorem Complexity.DecisionTree.On.assignmentFor_applyTo {N : ℕ} (queries : List (Fin N)) (input : BitString N) : (assignmentFor queries input).applyTo input = input

Reapplying values read from an input leaves that input unchanged.

theorem Complexity.DecisionTree.On.assignmentFor_reapply {N : ℕ} (queries : List (Fin N)) (input fallback : BitString N) : assignmentFor queries ((assignmentFor queries input).applyTo fallback) = assignmentFor queries input

Reading a query block back from any total extension of the induced restriction recovers the same restriction.

theorem Complexity.DecisionTree.On.assignmentOfPath_append {N : ℕ} (left right : List (Fin N × Bool)) : assignmentOfPath (left ++ right) = (assignmentOfPath left).comp (assignmentOfPath right)

Concatenating path records composes their induced restrictions.

theorem Complexity.DecisionTree.On.assignmentOfPath_apply_of_not_mem {N : ℕ} (path : List (Fin N × Bool)) (index : Fin N) (hindex : index ∉ List.map Prod.fst path) : assignmentOfPath path index = none

A path assignment leaves every unrecorded coordinate free.

theorem Complexity.DecisionTree.On.assignmentOfPath_apply_eq_some_of_mem {N : ℕ} (path : List (Fin N × Bool)) (hnodup : (List.map Prod.fst path).Nodup) (index : Fin N) (hindex : index ∈ List.map Prod.fst path) : ∃ (value : Bool), assignmentOfPath path index = some value

Every coordinate recorded by a duplicate-free path receives a value.

theorem Complexity.DecisionTree.On.assignmentOfPath_apply_of_mem {N : ℕ} (path : List (Fin N × Bool)) (hnodup : (List.map Prod.fst path).Nodup) (query : Fin N × Bool) (hquery : query ∈ path) : assignmentOfPath path query.1 = some query.2

A query/value pair in a duplicate-free path is recorded exactly.

theorem Complexity.DecisionTree.On.assignmentOfPath_deepBlockPath {N : ℕ} (queries : List (Fin N)) (continuation : Restriction.On N → On N) : assignmentOfPath (deepBlockPath queries continuation) = deepBranch queries continuation

The path record selected through a complete block induces exactly the selected deep-branch restriction.

theorem Complexity.DecisionTree.On.deepPath_queryAll {N : ℕ} (queries : List (Fin N)) (continuation : Restriction.On N → On N) : (queryAll queries continuation).deepPath = deepBlockPath queries continuation ++ (continuation (deepBranch queries continuation)).deepPath

The canonical deepest path through a complete block consists of the block prefix followed by the deepest path of the selected continuation.

theorem Complexity.DecisionTree.On.map_fst_deepBlockPath {N : ℕ} (queries : List (Fin N)) (continuation : Restriction.On N → On N) : List.map Prod.fst (deepBlockPath queries continuation) = queries

The block portion of the canonical deepest path queries exactly the listed coordinates, in order.

theorem Complexity.DecisionTree.On.deepBranch_apply_of_not_mem {N : ℕ} (queries : List (Fin N)) (continuation : Restriction.On N → On N) (index : Fin N) (hmem : index ∉ queries) : deepBranch queries continuation index = none

The selected deep branch leaves every coordinate outside the block free.

theorem Complexity.DecisionTree.On.deepBranch_apply_eq_some_of_mem {N : ℕ} (queries : List (Fin N)) (continuation : Restriction.On N → On N) (hnodup : queries.Nodup) (index : Fin N) (hmem : index ∈ queries) : ∃ (value : Bool), deepBranch queries continuation index = some value

Every coordinate in a duplicate-free block is fixed by the selected deep branch.

theorem Complexity.DecisionTree.On.deepBranch_apply_of_mem_deepBlockPath {N : ℕ} (queries : List (Fin N)) (continuation : Restriction.On N → On N) (hnodup : queries.Nodup) (query : Fin N × Bool) (hquery : query ∈ deepBlockPath queries continuation) : deepBranch queries continuation query.1 = some query.2

The selected restriction records every query/value pair in the canonical deep block path.

theorem Complexity.DecisionTree.On.assignmentFor_deepBranch {N : ℕ} (queries : List (Fin N)) (continuation : Restriction.On N → On N) (hnodup : queries.Nodup) (fallback : BitString N) : assignmentFor queries ((deepBranch queries continuation).applyTo fallback) = deepBranch queries continuation

Canonicalizing a duplicate-free selected deep branch by reading it back from any total extension changes nothing.

theorem Complexity.DecisionTree.On.eval_queryAll {N : ℕ} (queries : List (Fin N)) (continuation : Restriction.On N → On N) (input : BitString N) : eval input (queryAll queries continuation) = eval input (continuation (assignmentFor queries input))

Query-block evaluation passes the restriction read from the input to the continuation.

theorem Complexity.DecisionTree.On.depth_queryAll_le {N : ℕ} (queries : List (Fin N)) (continuation : Restriction.On N → On N) (continuationDepth : ℕ) (hdepth : ∀ (restriction : Restriction.On N), (continuation restriction).depth ≤ continuationDepth) : (queryAll queries continuation).depth ≤ queries.length + continuationDepth

A query block adds at most its list length to a uniform continuation-depth bound.

theorem Complexity.DecisionTree.On.vars_queryAll_subset {N : ℕ} (queries : List (Fin N)) (continuation : Restriction.On N → On N) (support : Finset (Fin N)) (hvars : ∀ (restriction : Restriction.On N), (continuation restriction).vars ⊆ support) : (queryAll queries continuation).vars ⊆ queries.toFinset ∪ support

Query-block support consists only of the listed queries and continuation support.

theorem Complexity.DecisionTree.On.pathReadOnce_queryAll {N : ℕ} (queries : List (Fin N)) (continuation : Restriction.On N → On N) (hnodup : queries.Nodup) (hreadOnce : ∀ (restriction : Restriction.On N), (continuation restriction).PathReadOnce) (hdisjoint : ∀ (restriction : Restriction.On N), Disjoint queries.toFinset (continuation restriction).vars) : (queryAll queries continuation).PathReadOnce

Distinct block queries followed by read-once continuations on disjoint support form a path-read-once decision tree.