Decoder-facing combined switching advice

This module gives the counted block advice a canonical sequential interpretation. Each stored position subset is replayed in increasing source order. A continuing block closes after its last query, while the last block never needs a closing marker because replay ends with the advice list.

def Algebraic.AC0.Switching.BlockAdvice.toQueryList {width length : ℕ} (block : BlockAdvice width length) (closesBlock : Bool) : List (QueryAdvice width)

Expand one block into the elementary query format used by the canonical replay decoder.

Equations

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

@[simp]

theorem Algebraic.AC0.Switching.BlockAdvice.length_toQueryList {width length : ℕ} (block : BlockAdvice width length) (closesBlock : Bool) : (block.toQueryList closesBlock).length = length

Expanding a block preserves its indexed length.

def Algebraic.AC0.Switching.CombinedAdvice.SuccView (width pathLength : ℕ) : Type

Combined advice for a nonempty path, split into its first block and, if that block does not end the path, the advice for the rest.

Equations

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

def Algebraic.AC0.Switching.CombinedAdvice.succEquiv (width pathLength : ℕ) : CombinedAdvice width pathLength.succ ≃ SuccView width pathLength

Combined advice for a path of length pathLength + 1 is its first-block view.

Equations

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

@[irreducible]

def Algebraic.AC0.Switching.CombinedAdvice.toQueryList {width : ℕ} (pathLength : ℕ) : CombinedAdvice width pathLength → List (QueryAdvice width)

Flatten combined advice into sequential query advice. Source positions are sorted within each block; exactly the nonfinal block boundaries are marked.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.AC0.Switching.CombinedAdvice.toQueryList 0 x_2 = []

@[simp]

theorem Algebraic.AC0.Switching.CombinedAdvice.length_toQueryList {width pathLength : ℕ} (advice : CombinedAdvice width pathLength) : (toQueryList pathLength advice).length = pathLength

Flattening combined advice produces exactly the indexed number of query symbols.

def Algebraic.AC0.Switching.CombinedAdvice.finalView {width remaining : ℕ} (block : BlockAdvice width (remaining + 1)) (lengthLeWidth : remaining + 1 ≤ width) : SuccView width remaining

The first-block view of advice consisting of one final block.

Equations

• Algebraic.AC0.Switching.CombinedAdvice.finalView block lengthLeWidth = ⟨⟨remaining, ⋯⟩, ⋯.mpr block⟩

def Algebraic.AC0.Switching.CombinedAdvice.ofFinalBlock {width remaining : ℕ} (block : BlockAdvice width (remaining + 1)) (lengthLeWidth : remaining + 1 ≤ width) : CombinedAdvice width (remaining + 1)

Package one positive-length block as final combined advice.

Equations

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

@[simp]

theorem Algebraic.AC0.Switching.CombinedAdvice.toQueryList_ofFinalBlock {width remaining : ℕ} (block : BlockAdvice width (remaining + 1)) (lengthLeWidth : remaining + 1 ≤ width) : toQueryList (remaining + 1) (ofFinalBlock block lengthLeWidth) = block.toQueryList false

Flattening a packaged final block returns precisely that block, with no operationally unnecessary closing marker.

def Algebraic.AC0.Switching.CombinedAdvice.prependView {width blockRemaining tailLength : ℕ} (block : ContinuingBlockAdvice width (blockRemaining + 1)) (tail : CombinedAdvice width tailLength) (blockLeWidth : blockRemaining + 1 ≤ width) (tailPositive : 0 < tailLength) : SuccView width (blockRemaining + tailLength)

The first-block view of advice obtained by prepending a continuing block to the advice for a nonempty remainder.

Equations

• Algebraic.AC0.Switching.CombinedAdvice.prependView block tail blockLeWidth tailPositive = ⟨⟨blockRemaining, ⋯⟩, have notFinal := ⋯; ⋯.mpr (block, ⋯ ▸ tail)⟩

def Algebraic.AC0.Switching.CombinedAdvice.prependBlock {width blockRemaining tailLength : ℕ} (block : ContinuingBlockAdvice width (blockRemaining + 1)) (tail : CombinedAdvice width tailLength) (blockLeWidth : blockRemaining + 1 ≤ width) (tailPositive : 0 < tailLength) : CombinedAdvice width (blockRemaining + tailLength).succ

Prepend a positive continuing block to nonempty combined advice.

Equations

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

@[simp]

theorem Algebraic.AC0.Switching.CombinedAdvice.toQueryList_prependBlock {width blockRemaining tailLength : ℕ} (block : ContinuingBlockAdvice width (blockRemaining + 1)) (tail : CombinedAdvice width tailLength) (blockLeWidth : blockRemaining + 1 ≤ width) (tailPositive : 0 < tailLength) : toQueryList (blockRemaining + tailLength).succ (prependBlock block tail blockLeWidth tailPositive) = (↑block).toQueryList true ++ toQueryList tailLength tail

Flattening prepended advice concatenates the continuing block and the nonempty tail.

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

The same query advice with its block-closing marker cleared.

Equations

• advice.withoutClose = { position := advice.position, closesBlock := false, difference := advice.difference }

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

Erase the final query's block-closing marker. It is operationally irrelevant because no advice remains after that query.

Equations

• Algebraic.AC0.Switching.clearLastClose [] = []
• Algebraic.AC0.Switching.clearLastClose [advice] = [advice.withoutClose]
• Algebraic.AC0.Switching.clearLastClose (advice :: next :: rest) = advice :: Algebraic.AC0.Switching.clearLastClose (next :: rest)

@[simp]

theorem Algebraic.AC0.Switching.length_clearLastClose {width : ℕ} (advice : List (QueryAdvice width)) : (clearLastClose advice).length = advice.length

Erasing the last closing marker preserves list length.

theorem Algebraic.AC0.Switching.replayIndices_clearLastClose {n width : ℕ} (formula : DNF n) (state : PartialAssignment n) (currentTerm : Option (Term n)) (advice : List (QueryAdvice width)) : replayIndices formula state currentTerm (clearLastClose advice) = replayIndices formula state currentTerm advice

Canonical replay is insensitive to the final query's closing marker.

def Algebraic.AC0.Switching.decodeCombined {n width pathLength : ℕ} (formula : DNF n) (encoded : PartialAssignment n × CombinedAdvice width pathLength) : PartialAssignment n

Decode a refined restriction carrying combined block advice.

Equations

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