Canonical traces as combined switching blocks

This module extracts the source-term block structure of a canonical DNF path. Each raw block stores increasing source positions and path bits relative to the values satisfying the selected term. Every nonfinal block is proved to contain a mismatch: without one, that term would remain the first surviving term after its last live variable was fixed, so canonical selection could not start a later nonempty block.

The result is the structural input to the counted combined advice type. No formulas, paths, assignments, or circuits are enumerated here.

@[reducible, inline]

abbrev Algebraic.AC0.Switching.RelativeQuery (width : ℕ) : Type

Position and relative path bit before a block boundary is synthesized.

Equations

• Algebraic.AC0.Switching.RelativeQuery width = (Fin width × Bool)

def Algebraic.AC0.Switching.QueryAdvice.toRelativeQuery {width : ℕ} (advice : QueryAdvice width) : RelativeQuery width

Forget the block-boundary bit of elementary query advice.

Equations

• advice.toRelativeQuery = (advice.position, advice.difference)

def Algebraic.AC0.Switching.RelativeBlockHasMismatch {width : ℕ} (block : List (RelativeQuery width)) : Prop

A raw source-term block contains a path value that falsifies one of the selected term's literals.

Equations

• Algebraic.AC0.Switching.RelativeBlockHasMismatch block = ∃ query ∈ block, query.2 = true

def Algebraic.AC0.Switching.RelativeBlocksHaveContinuingMismatch {width : ℕ} : List (List (RelativeQuery width)) → Prop

Every block except the last has a relative path mismatch.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.AC0.Switching.RelativeBlocksHaveContinuingMismatch [] = True
• Algebraic.AC0.Switching.RelativeBlocksHaveContinuingMismatch [head] = True

def Algebraic.AC0.Switching.prependToFirstBlock {α : Type u_1} (query : α) : List (List α) → List (List α)

Prepend a query to the first block, creating that block when necessary.

Equations

• Algebraic.AC0.Switching.prependToFirstBlock query [] = [[query]]
• Algebraic.AC0.Switching.prependToFirstBlock query (block :: rest) = (query :: block) :: rest

def Algebraic.AC0.DNF.CanonicalTrace.combinedBlocks {widthBound n : ℕ} [NeZero widthBound] {formula : DNF n} {rho : PartialAssignment n} {steps : List (DecisionTree.PathStep n)} (trace : formula.CanonicalTrace rho steps) : List (List (Switching.RelativeQuery widthBound))

Partition a canonical trace into maximal source-term blocks.

Equations

• (Algebraic.AC0.DNF.CanonicalTrace.nil rho).combinedBlocks = []
• (Algebraic.AC0.DNF.CanonicalTrace.start found support_eq nonempty block).combinedBlocks = block.combinedBlocks

def Algebraic.AC0.DNF.CanonicalBlockTrace.combinedBlocks {widthBound n : ℕ} [NeZero widthBound] {formula : DNF n} {term : Term n} {rho : PartialAssignment n} {indices : List (Fin n)} {steps : List (DecisionTree.PathStep n)} (trace : formula.CanonicalBlockTrace term rho indices steps) : List (List (Switching.RelativeQuery widthBound))

Partition the remaining part of a canonical source-term traversal.

Equations

• One or more equations did not get rendered due to their size.
• (Algebraic.AC0.DNF.CanonicalBlockTrace.nil rho index rest).combinedBlocks = []

theorem Algebraic.AC0.DNF.CanonicalTrace.flatten_combinedBlocks {widthBound n : ℕ} [NeZero widthBound] {formula : DNF n} {rho : PartialAssignment n} {steps : List (DecisionTree.PathStep n)} (trace : formula.CanonicalTrace rho steps) : trace.combinedBlocks.flatten = List.map Switching.QueryAdvice.toRelativeQuery trace.adviceList

Flattening raw blocks forgets exactly the boundary bit of elementary canonical advice.

theorem Algebraic.AC0.DNF.CanonicalBlockTrace.flatten_combinedBlocks {widthBound n : ℕ} [NeZero widthBound] {formula : DNF n} {term : Term n} {rho : PartialAssignment n} {indices : List (Fin n)} {steps : List (DecisionTree.PathStep n)} (trace : formula.CanonicalBlockTrace term rho indices steps) : trace.combinedBlocks.flatten = List.map Switching.QueryAdvice.toRelativeQuery trace.adviceList

The same flattening correspondence inside one source-term block.

theorem Algebraic.AC0.DNF.CanonicalTrace.combinedBlocks_nonempty {widthBound n : ℕ} [NeZero widthBound] {formula : DNF n} {rho : PartialAssignment n} {steps : List (DecisionTree.PathStep n)} (trace : formula.CanonicalTrace rho steps) (block : List (Switching.RelativeQuery widthBound)) : block ∈ trace.combinedBlocks → block ≠ []

Every raw block extracted from a canonical trace is nonempty.

theorem Algebraic.AC0.DNF.CanonicalBlockTrace.combinedBlocks_nonempty {widthBound n : ℕ} [NeZero widthBound] {formula : DNF n} {term : Term n} {rho : PartialAssignment n} {indices : List (Fin n)} {steps : List (DecisionTree.PathStep n)} (trace : formula.CanonicalBlockTrace term rho indices steps) (block : List (Switching.RelativeQuery widthBound)) : block ∈ trace.combinedBlocks → block ≠ []

The same nonemptiness invariant inside one source-term traversal.

theorem Algebraic.AC0.DNF.CanonicalTrace.sum_length_combinedBlocks {widthBound n : ℕ} [NeZero widthBound] {formula : DNF n} {rho : PartialAssignment n} {steps : List (DecisionTree.PathStep n)} (trace : formula.CanonicalTrace rho steps) : (List.map List.length trace.combinedBlocks).sum = steps.length

Canonical block decomposition partitions every query exactly once.

theorem Algebraic.AC0.DNF.CanonicalBlockTrace.firstBlock_positions_sublist {widthBound n : ℕ} [NeZero widthBound] {formula : DNF n} {term : Term n} {rho : PartialAssignment n} {indices : List (Fin n)} {steps : List (DecisionTree.PathStep n)} (trace : formula.CanonicalBlockTrace term rho indices steps) (block : List (Switching.RelativeQuery widthBound)) (blocks : List (List (Switching.RelativeQuery widthBound))) : trace.combinedBlocks = block :: blocks → (List.map Prod.fst block).Sublist (List.map (LiteralSet.sourcePosition term) indices)

Positions in the first raw block form a sublist of the selected term's remaining source positions.

theorem Algebraic.AC0.DNF.CanonicalTrace.combinedBlocks_positions_pairwise {widthBound n : ℕ} [NeZero widthBound] {formula : DNF n} {rho : PartialAssignment n} {steps : List (DecisionTree.PathStep n)} (trace : formula.CanonicalTrace rho steps) (bounded : formula.WidthAtMost widthBound) (block : List (Switching.RelativeQuery widthBound)) : block ∈ trace.combinedBlocks → List.Pairwise (fun (x1 x2 : Fin widthBound) => x1 < x2) (List.map Prod.fst block)

Source positions are strictly increasing within every canonical block.

theorem Algebraic.AC0.DNF.CanonicalBlockTrace.combinedBlocks_positions_pairwise {widthBound n : ℕ} [NeZero widthBound] {formula : DNF n} {term : Term n} {rho : PartialAssignment n} {indices : List (Fin n)} {steps : List (DecisionTree.PathStep n)} (trace : formula.CanonicalBlockTrace term rho indices steps) (bounded : formula.WidthAtMost widthBound) (termBound : LiteralSet.width term ≤ widthBound) (supportEq : liveSupport term rho = indices) (block : List (Switching.RelativeQuery widthBound)) : block ∈ trace.combinedBlocks → List.Pairwise (fun (x1 x2 : Fin widthBound) => x1 < x2) (List.map Prod.fst block)

The same strict source-order invariant inside one source-term traversal.

theorem Algebraic.AC0.DNF.CanonicalTrace.combinedBlock_length_le_width {widthBound n : ℕ} [NeZero widthBound] {formula : DNF n} {rho : PartialAssignment n} {steps : List (DecisionTree.PathStep n)} (trace : formula.CanonicalTrace rho steps) (bounded : formula.WidthAtMost widthBound) {block : List (Switching.RelativeQuery widthBound)} (present : block ∈ trace.combinedBlocks) : block.length ≤ widthBound

Every canonical block contains at most the declared source width.

def Algebraic.AC0.DNF.CanonicalBlockTrace.currentRelativeBlock {widthBound n : ℕ} [NeZero widthBound] {formula : DNF n} {term : Term n} {rho : PartialAssignment n} {indices : List (Fin n)} {steps : List (DecisionTree.PathStep n)} (trace : formula.CanonicalBlockTrace term rho indices steps) : List (Switching.RelativeQuery widthBound)

Queries remaining in the source-term block currently being traversed.

Equations

• (Algebraic.AC0.DNF.CanonicalBlockTrace.nil rho index rest).currentRelativeBlock = []
• tail.takeMore.currentRelativeBlock = (Algebraic.AC0.LiteralSet.sourcePosition term index, Algebraic.AC0.LiteralSet.satisfyingValue term index ^^ value) :: tail.currentRelativeBlock
• (Algebraic.AC0.DNF.CanonicalBlockTrace.takeLast tail).currentRelativeBlock = [(Algebraic.AC0.LiteralSet.sourcePosition term index, Algebraic.AC0.LiteralSet.satisfyingValue term index ^^ value)]

def Algebraic.AC0.DNF.CanonicalBlockTrace.followingRelativeBlocks {widthBound n : ℕ} [NeZero widthBound] {formula : DNF n} {term : Term n} {rho : PartialAssignment n} {indices : List (Fin n)} {steps : List (DecisionTree.PathStep n)} (trace : formula.CanonicalBlockTrace term rho indices steps) : List (List (Switching.RelativeQuery widthBound))

Complete source-term blocks following the block currently traversed.

Equations

• (Algebraic.AC0.DNF.CanonicalBlockTrace.nil rho index rest).followingRelativeBlocks = []
• tail.takeMore.followingRelativeBlocks = tail.followingRelativeBlocks
• (Algebraic.AC0.DNF.CanonicalBlockTrace.takeLast tail).followingRelativeBlocks = tail.combinedBlocks

theorem Algebraic.AC0.DNF.CanonicalBlockTrace.combinedBlocks_eq_current_cons_following {widthBound n : ℕ} [NeZero widthBound] {formula : DNF n} {term : Term n} {rho : PartialAssignment n} {indices : List (Fin n)} {steps : List (DecisionTree.PathStep n)} (trace : formula.CanonicalBlockTrace term rho indices steps) : trace.combinedBlocks = match trace.currentRelativeBlock with | [] => [] | block => block :: trace.followingRelativeBlocks

The direct block decomposition is the current nonempty block followed by the blocks reached after its boundary.

theorem Algebraic.AC0.DNF.CanonicalBlockTrace.currentRelativeBlock_hasMismatch_of_following {widthBound n : ℕ} [NeZero widthBound] {formula : DNF n} {term : Term n} {rho : PartialAssignment n} {indices : List (Fin n)} {steps : List (DecisionTree.PathStep n)} (trace : formula.CanonicalBlockTrace term rho indices steps) (found : formula.firstSurviving rho = some term) (supportEq : liveSupport term rho = indices) (hasFollowing : trace.followingRelativeBlocks ≠ []) : Switching.RelativeBlockHasMismatch trace.currentRelativeBlock

A completed current block must contain a falsifying relative bit whenever canonical selection proceeds to a later block.

theorem Algebraic.AC0.DNF.CanonicalTrace.combinedBlocks_haveContinuingMismatch {widthBound n : ℕ} [NeZero widthBound] {formula : DNF n} {rho : PartialAssignment n} {steps : List (DecisionTree.PathStep n)} (trace : formula.CanonicalTrace rho steps) : Switching.RelativeBlocksHaveContinuingMismatch trace.combinedBlocks

Every nonfinal block extracted from a canonical trace has a mismatch.

theorem Algebraic.AC0.DNF.CanonicalBlockTrace.followingRelativeBlocks_haveContinuingMismatch {widthBound n : ℕ} [NeZero widthBound] {formula : DNF n} {term : Term n} {rho : PartialAssignment n} {indices : List (Fin n)} {steps : List (DecisionTree.PathStep n)} (trace : formula.CanonicalBlockTrace term rho indices steps) : Switching.RelativeBlocksHaveContinuingMismatch trace.followingRelativeBlocks

Blocks reached after the current source term inherit the nonfinal mismatch property from their nested canonical traces.