Finite iteration of anti-checker selection rounds -- definitions

The counter family is indexed by the current labeled-prefix length. This module composes the corresponding width-changing state circuit for any bounded number of rounds, retaining exact types at every intermediate prefix length.

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.emptyLabeledPrefix (arity : ℕ) : BitString (0 * (arity + 1))

The empty row-major labeled-prefix encoding.

Equations

• Complexity.GapMCSP.Magnification.AntiCheckerLemma.emptyLabeledPrefix arity coordinate = ⟨↑coordinate, ⋯⟩.elim0

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.selectionEmptyStateInputMap (arity : ℕ) : Fin (selectionRoundInputWidth arity 0) → Fin (2 ^ arity)

Reindex the zero-round state width to the bare truth-table width.

Equations

• Complexity.GapMCSP.Magnification.AntiCheckerLemma.selectionEmptyStateInputMap arity input = ⟨↑input, ⋯⟩

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.selectionTraceState {arity rounds : ℕ} (target : BitString arity → Bool) (inputs : Fin rounds → BitString arity) : BitString (selectionRoundInputWidth arity rounds)

Circuit state represented by a target truth table and an ordered vector of target-labeled selected inputs.

Equations

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

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.selectionSampleOutputMap (arity rounds : ℕ) : Fin (rounds * arity) → Fin (selectionRoundInputWidth arity rounds)

Project the input coordinates from the labeled rows carried by a selection state, discarding the preserved truth table and every output label.

Equations

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

instance Complexity.GapMCSP.Magnification.AntiCheckerLemma.instNeZeroNatHMulRequiredRoundCount (beta : PositiveRationalScale) (arity : ℕ) [NeZero arity] : NeZero (requiredRoundCount beta arity * arity)

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.selectionPrefixPriorBound {beta : PositiveRationalScale} {arity rounds : ℕ} (hrounds : rounds + 1 ≤ requiredRoundCount beta arity) : rounds ≤ requiredRoundCount beta arity

Removing the final round preserves the required-round upper bound.

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.selectionPrefixCounterIndex {beta : PositiveRationalScale} {arity rounds : ℕ} (hrounds : rounds + 1 ≤ requiredRoundCount beta arity) : Fin (requiredRoundCount beta arity)

Counter-family index used by the final step of a nonempty bounded prefix.

Equations

• Complexity.GapMCSP.Magnification.AntiCheckerLemma.selectionPrefixCounterIndex hrounds = ⟨rounds, ⋯⟩

noncomputable def Complexity.GapMCSP.Magnification.AntiCheckerLemma.selectionPrefixCircuit {overhead arity : ℕ} {beta : PositiveRationalScale} (family : ApproximateCounterFamily overhead beta arity) (rounds : ℕ) : rounds ≤ requiredRoundCount beta arity → (internalGates : ℕ) × Circuit Basis.andOr2 (2 ^ arity) (selectionRoundInputWidth arity rounds) internalGates

Compose the first rounds counter-selection state transitions.

Equations

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

noncomputable def Complexity.GapMCSP.Magnification.AntiCheckerLemma.fullSelectionStateCircuit {overhead arity : ℕ} {beta : PositiveRationalScale} (family : ApproximateCounterFamily overhead beta arity) : (internalGates : ℕ) × Circuit Basis.andOr2 (2 ^ arity) (selectionRoundInputWidth arity (requiredRoundCount beta arity)) internalGates

State circuit after every required counter-selection round.

Equations

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

noncomputable def Complexity.GapMCSP.Magnification.AntiCheckerLemma.fullSelectionSamplesCircuit {overhead arity : ℕ} {beta : PositiveRationalScale} [NeZero arity] (family : ApproximateCounterFamily overhead beta arity) : (internalGates : ℕ) × Circuit Basis.andOr2 (2 ^ arity) (requiredRoundCount beta arity * arity) internalGates

Full selection circuit with its carried state projected down to the packed input coordinates of the required-round sample vector.

Equations

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