Finite circuit-code enumeration -- definitions

This layer gives the Anti-Checker Lemma's survivor count a canonical finite domain. It enumerates every bit string up to the polynomial encoding bound, then filters for canonical, well-formed circuit descriptions whose decoded gate count is within the requested threshold.

def Complexity.AntiChecker.codesOfLength (length : ℕ) : Finset (List Bool)

Every Boolean string of exactly length bits.

Equations

• Complexity.AntiChecker.codesOfLength length = Finset.image Complexity.BitString.toList Finset.univ

def Complexity.AntiChecker.codesUpTo (bound : ℕ) : Finset (List Bool)

Every Boolean string of length at most bound.

Equations

• Complexity.AntiChecker.codesUpTo bound = (Finset.range (bound + 1)).biUnion Complexity.AntiChecker.codesOfLength

def Complexity.AntiChecker.codeLengthBound (arity threshold : ℕ) : ℕ

Uniform encoding-length bound for circuits at one input arity and size threshold.

Equations

• Complexity.AntiChecker.codeLengthBound arity threshold = 1 + threshold * (2 * (arity + threshold) + 6)

def Complexity.AntiChecker.IsSmallCircuitCode (arity threshold : ℕ) (code : List Bool) : Prop

A canonical code for a well-formed circuit at the supplied arity whose decoded gate count is within the threshold.

Equations

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

@[instance_reducible]

instance Complexity.AntiChecker.instDecidableIsSmallCircuitCode (arity threshold : ℕ) (code : List Bool) : Decidable (IsSmallCircuitCode arity threshold code)

Equations

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

def Complexity.AntiChecker.candidateCodes (arity threshold : ℕ) : Finset (List Bool)

All canonical small-circuit codes inside the uniform encoding-length bound.

Equations

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