Packing canonical blocks into combined switching advice

This module turns the ordered raw blocks extracted from a canonical DNF trace into the finite CombinedAdvice type used by the sharp counting argument. It proves exact correspondence with the elementary replay transcript, including synthesized block boundaries, and obtains a replay-and-clear left inverse for every bounded canonical path.

def Algebraic.AC0.Switching.BlockAdvice.ofRelativeBlock {width : ℕ} (block : List (RelativeQuery width)) (positionsSorted : List.Pairwise (fun (x1 x2 : Fin width) => x1 < x2) (List.map Prod.fst block)) : BlockAdvice width block.length

Convert one ordered raw block into indexed counted advice.

Equations

• One or more equations did not get rendered due to their size.

def Algebraic.AC0.Switching.RelativeQuery.toQueryAdvice {width : ℕ} (query : RelativeQuery width) (closesBlock : Bool) : QueryAdvice width

Restore an elementary query symbol from its relative position and bit.

Equations

• query.toQueryAdvice closesBlock = { position := query.1, closesBlock := closesBlock, difference := query.2 }

def Algebraic.AC0.Switching.relativeBlockToQueryList {width : ℕ} (block : List (RelativeQuery width)) (closesBlock : Bool) : List (QueryAdvice width)

Add the boundary convention expected by the elementary replay decoder to one raw block.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Algebraic.AC0.Switching.relativeBlockToQueryList_singleton {width : ℕ} (query : RelativeQuery width) (closesBlock : Bool) : relativeBlockToQueryList [query] closesBlock = [query.toQueryAdvice closesBlock]

A singleton raw block receives precisely the requested boundary bit.

theorem Algebraic.AC0.Switching.BlockAdvice.toQueryList_ofRelativeBlock {width : ℕ} (block : List (RelativeQuery width)) (positionsSorted : List.Pairwise (fun (x1 x2 : Fin width) => x1 < x2) (List.map Prod.fst block)) (closesBlock : Bool) : (ofRelativeBlock block positionsSorted).toQueryList closesBlock = relativeBlockToQueryList block closesBlock

Expanding a counted block constructed from raw data recovers the exact elementary query list, including the chosen final boundary marker.

theorem Algebraic.AC0.Switching.BlockAdvice.map_toRelativeQuery_toQueryList_ofRelativeBlock {width : ℕ} (block : List (RelativeQuery width)) (positionsSorted : List.Pairwise (fun (x1 x2 : Fin width) => x1 < x2) (List.map Prod.fst block)) (closesBlock : Bool) : List.map QueryAdvice.toRelativeQuery ((ofRelativeBlock block positionsSorted).toQueryList closesBlock) = block

Re-expanding a raw block recovers its positions and differences; the chosen closing bit is deliberately forgotten.

theorem Algebraic.AC0.Switching.BlockAdvice.hasMismatch_ofRelativeBlock {width : ℕ} (block : List (RelativeQuery width)) (positionsSorted : List.Pairwise (fun (x1 x2 : Fin width) => x1 < x2) (List.map Prod.fst block)) (mismatch : RelativeBlockHasMismatch block) : (ofRelativeBlock block positionsSorted).HasMismatch

A raw mismatch becomes exactly the nonzero-difference condition required by a continuing counted block.

def Algebraic.AC0.Switching.relativeBlocksToQueryList {width : ℕ} : List (List (RelativeQuery width)) → List (QueryAdvice width)

Sequential elementary advice represented by a list of relative blocks. Every nonfinal block receives a closing marker; the final block does not.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.AC0.Switching.relativeBlocksToQueryList [] = []
• Algebraic.AC0.Switching.relativeBlocksToQueryList [block] = Algebraic.AC0.Switching.relativeBlockToQueryList block false

structure Algebraic.AC0.Switching.RelativeBlockPacking (width : ℕ) (blocks : List (List (RelativeQuery width))) : Type

Counted combined advice together with its exact elementary replay list.

• advice : CombinedAdvice width (List.map List.length blocks).sum

  Counted advice occupying the sum of the raw block lengths.

• toQueryList : CombinedAdvice.toQueryList (List.map List.length blocks).sum self.advice = relativeBlocksToQueryList blocks

  Re-expansion produces exactly the boundary-annotated raw blocks.

def Algebraic.AC0.Switching.packRelativeBlocks {width : ℕ} (blocks : List (List (RelativeQuery width))) (nonempty : ∀ block ∈ blocks, block ≠ []) (positionsSorted : ∀ block ∈ blocks, List.Pairwise (fun (x1 x2 : Fin width) => x1 < x2) (List.map Prod.fst block)) (lengthLeWidth : ∀ block ∈ blocks, block.length ≤ width) (continuingMismatch : RelativeBlocksHaveContinuingMismatch blocks) : RelativeBlockPacking width blocks

Recursively package structurally valid raw blocks, retaining the exact replay-list equation as part of the construction.

Equations

• One or more equations did not get rendered due to their size.

def Algebraic.AC0.Switching.CombinedAdvice.ofRelativeBlocks {width : ℕ} (blocks : List (List (RelativeQuery width))) (nonempty : ∀ block ∈ blocks, block ≠ []) (positionsSorted : ∀ block ∈ blocks, List.Pairwise (fun (x1 x2 : Fin width) => x1 < x2) (List.map Prod.fst block)) (lengthLeWidth : ∀ block ∈ blocks, block.length ≤ width) (continuingMismatch : RelativeBlocksHaveContinuingMismatch blocks) : CombinedAdvice width (List.map List.length blocks).sum

Package a structurally valid list of raw blocks as counted combined advice.

Equations

• One or more equations did not get rendered due to their size.

theorem Algebraic.AC0.Switching.CombinedAdvice.toQueryList_ofRelativeBlocks {width : ℕ} (blocks : List (List (RelativeQuery width))) (nonempty : ∀ block ∈ blocks, block ≠ []) (positionsSorted : ∀ block ∈ blocks, List.Pairwise (fun (x1 x2 : Fin width) => x1 < x2) (List.map Prod.fst block)) (lengthLeWidth : ∀ block ∈ blocks, block.length ≤ width) (continuingMismatch : RelativeBlocksHaveContinuingMismatch blocks) : toQueryList (List.map List.length blocks).sum (ofRelativeBlocks blocks nonempty positionsSorted lengthLeWidth continuingMismatch) = relativeBlocksToQueryList blocks

Packaging raw blocks preserves their exact sequential replay advice.

theorem Algebraic.AC0.DNF.CanonicalTrace.combinedBlocks_eq_nil_iff_adviceList_eq_nil {widthBound n : ℕ} [NeZero widthBound] {formula : DNF n} {rho : PartialAssignment n} {steps : List (DecisionTree.PathStep n)} (trace : formula.CanonicalTrace rho steps) : trace.combinedBlocks = [] ↔ trace.adviceList = []

A canonical raw-block sequence is empty exactly when its elementary advice transcript is empty.

theorem Algebraic.AC0.DNF.CanonicalTrace.relativeBlocksToQueryList_combinedBlocks {widthBound n : ℕ} [NeZero widthBound] {formula : DNF n} {rho : PartialAssignment n} {steps : List (DecisionTree.PathStep n)} (trace : formula.CanonicalTrace rho steps) : Switching.relativeBlocksToQueryList trace.combinedBlocks = Switching.clearLastClose trace.adviceList

Rebuilding elementary advice from canonical raw blocks gives the original transcript with its operationally irrelevant final closing marker cleared.

theorem Algebraic.AC0.DNF.CanonicalBlockTrace.relativeBlocksToQueryList_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) : Switching.relativeBlocksToQueryList trace.combinedBlocks = Switching.clearLastClose trace.adviceList

The same exact reconstruction while traversing one source term.

def Algebraic.AC0.DNF.CanonicalTrace.combinedAdvice {widthBound n : ℕ} [NeZero widthBound] {formula : DNF n} {rho : PartialAssignment n} {steps : List (DecisionTree.PathStep n)} (trace : formula.CanonicalTrace rho steps) (bounded : formula.WidthAtMost widthBound) : Switching.CombinedAdvice widthBound steps.length

Counted combined advice extracted from a bounded canonical trace.

Equations

• trace.combinedAdvice bounded = ⋯ ▸ Algebraic.AC0.Switching.CombinedAdvice.ofRelativeBlocks trace.combinedBlocks ⋯ ⋯ ⋯ ⋯

theorem Algebraic.AC0.DNF.CanonicalTrace.toQueryList_combinedAdvice {widthBound n : ℕ} [NeZero widthBound] {formula : DNF n} {rho : PartialAssignment n} {steps : List (DecisionTree.PathStep n)} (trace : formula.CanonicalTrace rho steps) (bounded : formula.WidthAtMost widthBound) : Switching.CombinedAdvice.toQueryList steps.length (trace.combinedAdvice bounded) = Switching.clearLastClose trace.adviceList

Listing a trace's counted combined advice recovers its elementary advice with only the final, operationally irrelevant closing marker cleared.

def Algebraic.AC0.DNF.CanonicalTrace.combinedAdviceOfLength {widthBound n : ℕ} [NeZero widthBound] {formula : DNF n} {rho : PartialAssignment n} {steps : List (DecisionTree.PathStep n)} {pathLength : ℕ} (trace : formula.CanonicalTrace rho steps) (bounded : formula.WidthAtMost widthBound) (lengthEq : steps.length = pathLength) : Switching.CombinedAdvice widthBound pathLength

Reindex counted trace advice by an externally prescribed path length.

Equations

• trace.combinedAdviceOfLength bounded lengthEq = lengthEq ▸ trace.combinedAdvice bounded

theorem Algebraic.AC0.DNF.CanonicalTrace.toQueryList_combinedAdviceOfLength {widthBound n : ℕ} [NeZero widthBound] {formula : DNF n} {rho : PartialAssignment n} {steps : List (DecisionTree.PathStep n)} {pathLength : ℕ} (trace : formula.CanonicalTrace rho steps) (bounded : formula.WidthAtMost widthBound) (lengthEq : steps.length = pathLength) : Switching.CombinedAdvice.toQueryList pathLength (trace.combinedAdviceOfLength bounded lengthEq) = Switching.clearLastClose trace.adviceList

Reindexing does not change the combined replay list.

theorem Algebraic.AC0.DNF.CanonicalTrace.replayIndices_combinedAdviceOfLength {widthBound n : ℕ} [NeZero widthBound] {formula : DNF n} {rho : PartialAssignment n} {steps : List (DecisionTree.PathStep n)} {pathLength : ℕ} (trace : formula.CanonicalTrace rho steps) (bounded : formula.WidthAtMost widthBound) (lengthEq : steps.length = pathLength) : Switching.replayIndices formula (rho.refine trace.satisfyingAssignment) none (Switching.CombinedAdvice.toQueryList pathLength (trace.combinedAdviceOfLength bounded lengthEq)) = DecisionTree.PathStep.indices steps

Combined advice replays exactly the original canonical path coordinates.

theorem Algebraic.AC0.DNF.CanonicalPath.decodeCombined_satisfyingEncoding {widthBound n : ℕ} [NeZero widthBound] {formula : DNF n} {rho : PartialAssignment n} {pathLength : ℕ} (path : formula.CanonicalPath rho pathLength) (trace : formula.CanonicalTrace rho path.steps) (bounded : formula.WidthAtMost widthBound) : Switching.decodeCombined formula (rho.refine trace.satisfyingAssignment, trace.combinedAdviceOfLength bounded ⋯) = rho

The combined replay-and-clear decoder is a left inverse of every valid canonical path encoding.