Finite anti-checkers -- definitions

An anti-checker for a target function is a finite list of inputs that catches every circuit up to a chosen size threshold: each such circuit disagrees with the target on at least one listed input. Lists are the concrete multiset representation used by the later generator. Repetitions and order are retained syntactically but do not affect the semantic predicate.

This first layer is for positive arity, matching the hardness-magnification application. SuccinctMCSP separately gives its zero-arity convention.

def Complexity.AntiChecker.AgreesOn {arity internalGates : ℕ} [NeZero arity] (circuit : Circuit Basis.andOr2 arity 1 internalGates) (target : BitString arity → Bool) (inputs : List (BitString arity)) : Prop

A circuit agrees with the target on every input in the finite list.

Equations

• Complexity.AntiChecker.AgreesOn circuit target inputs = ∀ input ∈ inputs, circuit.eval input 0 = target input

def Complexity.AntiChecker.IsFor {arity : ℕ} [NeZero arity] (target : BitString arity → Bool) (threshold : ℕ) (inputs : List (BitString arity)) : Prop

A finite list is an anti-checker when it contains a counterexample to every circuit within the threshold.

Equations

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

def Complexity.AntiChecker.padInputsTo {arity : ℕ} (targetLength : ℕ) (inputs : List (BitString arity)) : List (BitString arity)

Prepend all-zero inputs until the list reaches targetLength. If the list is already at least that long, leave it unchanged.

Equations

• Complexity.AntiChecker.padInputsTo targetLength inputs = (List.replicate (targetLength - inputs.length) fun (x : Fin arity) => false) ++ inputs