Combined block advice for the switching lemma

This module isolates the finite counting argument that improves the elementary one-position/two-bit switching encoding. Following the combined encoding in Beame's A Switching Lemma Primer, a term block records an unordered subset of source-term positions and the path bits relative to the assignment satisfying that term. Every block followed by another block has a nonzero difference string; only the final block may use the all-zero string.

CombinedAdvice width pathLength packages exactly those block sequences. Its cardinality is at most ((5 * width - 1) / 2) ^ pathLength for positive width. This is an abstract structural count: it does not enumerate formulas, paths, or circuits.

structure Algebraic.AC0.Switching.BlockAdvice (width length : ℕ) : Type

Advice for one source-term block. Positions form a subset because the canonical path queries them in source order; sorting the subset recovers that order. Each Boolean says whether the path value differs from the value that satisfies the corresponding literal.

• positions : { set : Finset (Fin width) // set.card = length }

  Queried source-term positions.

• differences : Fin length → Bool

  Difference bits, indexed in increasing source-position order.

@[instance_reducible]

instance Algebraic.AC0.Switching.instDecidableEqBlockAdvice {width✝ length✝ : ℕ} : DecidableEq (BlockAdvice width✝ length✝)

Equations

• Algebraic.AC0.Switching.instDecidableEqBlockAdvice = Algebraic.AC0.Switching.instDecidableEqBlockAdvice.decEq

def Algebraic.AC0.Switching.instDecidableEqBlockAdvice.decEq {width✝ length✝ : ℕ} (x✝ x✝¹ : BlockAdvice width✝ length✝) : Decidable (x✝ = x✝¹)

Equations

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

def Algebraic.AC0.Switching.BlockAdvice.HasMismatch {width length : ℕ} (block : BlockAdvice width length) : Prop

A block has a mismatch when its path falsifies at least one of the source term's literals.

Equations

• block.HasMismatch = (block.differences ≠ fun (x : Fin length) => false)

@[reducible, inline]

abbrev Algebraic.AC0.Switching.ContinuingBlockAdvice (width length : ℕ) : Type

A nonfinal block, whose difference string must be nonzero before the canonical construction can move to a later source term.

Equations

• Algebraic.AC0.Switching.ContinuingBlockAdvice width length = { block : Algebraic.AC0.Switching.BlockAdvice width length // block.HasMismatch }

@[irreducible]

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

A sequence of source-term blocks occupying exactly pathLength queries. The last block is arbitrary; every block with a recursive tail is continuing and therefore carries a mismatch.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.AC0.Switching.CombinedAdvice width 0 = PUnit.{1}

@[instance_reducible]

noncomputable instance Algebraic.AC0.Switching.blockAdviceFintype {width length : ℕ} : Fintype (BlockAdvice width length)

The finite enumeration inherited from bounded position subsets and Boolean difference strings.

Equations

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

instance Algebraic.AC0.Switching.combinedAdviceFinite (width pathLength : ℕ) : Finite (CombinedAdvice width pathLength)

Proof-irrelevant finiteness obtained by strong induction on total path length.

@[instance_reducible]

noncomputable instance Algebraic.AC0.Switching.combinedAdviceFintype (width pathLength : ℕ) : Fintype (CombinedAdvice width pathLength)

Combined advice is finite at every path length.

Equations

• Algebraic.AC0.Switching.combinedAdviceFintype width pathLength = Fintype.ofFinite (Algebraic.AC0.Switching.CombinedAdvice width pathLength)

@[instance_reducible]

noncomputable instance Algebraic.AC0.Switching.continuingBlockAdviceFintype (width length : ℕ) : Fintype (ContinuingBlockAdvice width length)

Continuing blocks form a finite subtype of block advice.

Equations

• Algebraic.AC0.Switching.continuingBlockAdviceFintype width length = Fintype.ofFinite (Algebraic.AC0.Switching.ContinuingBlockAdvice width length)

theorem Algebraic.AC0.Switching.card_blockAdvice (width length : ℕ) : Fintype.card (BlockAdvice width length) = width.choose length * 2 ^ length

A length-length block chooses that many of the width positions and one Boolean difference bit per position.

theorem Algebraic.AC0.Switching.card_continuingBlockAdvice (width length : ℕ) : Fintype.card (ContinuingBlockAdvice width length) = width.choose length * (2 ^ length - 1)

Requiring a mismatch removes exactly the all-zero difference string.

theorem Algebraic.AC0.Switching.card_combinedAdvice_succ (width pathLength : ℕ) : Nat.card (CombinedAdvice width (pathLength + 1)) = ∑ index : Fin (width.min (pathLength + 1)), if ↑index = pathLength then width.choose (↑index + 1) * 2 ^ (↑index + 1) else width.choose (↑index + 1) * (2 ^ (↑index + 1) - 1) * Nat.card (CombinedAdvice width (pathLength - ↑index))

Exact first-block recurrence for the combined advice cardinality.

theorem Algebraic.AC0.Switching.natCard_combinedAdvice_cast_le (width pathLength : ℕ) (widthPositive : 0 < width) : ↑(Nat.card (CombinedAdvice width pathLength)) ≤ ((5 * ↑width - 1) / 2) ^ pathLength

Combined block advice has at most ((5 * width - 1) / 2)^pathLength elements. The subtraction occurs in Real, and positive width makes the base positive.

theorem Algebraic.AC0.Switching.card_combinedAdvice_cast_le (width pathLength : ℕ) (widthPositive : 0 < width) : ↑(Fintype.card (CombinedAdvice width pathLength)) ≤ ((5 * ↑width - 1) / 2) ^ pathLength

Fintype.card form of the combined-advice cardinality bound.