Fixed-width circuit-candidate enumeration -- definitions

This module gives the existing canonical small-circuit code set a finite type view. The proof layer identifies it exactly with valid fixed-width circuit descriptions at the same arity and gate threshold.

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

Canonical variable-length circuit codes in the existing finite candidate set, viewed as a finite type.

Equations

• Complexity.AntiChecker.CandidateCode arity threshold = Complexity.AntiChecker.candidateCodes arity threshold

@[instance_reducible]

instance Complexity.AntiChecker.instFintypeSubtypeListBoolMemFinsetCandidateCode (arity threshold : ℕ) : Fintype ↥(CandidateCode arity threshold)

Equations

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

@[instance_reducible]

instance Complexity.AntiChecker.instDecidableEqSubtypeListBoolMemFinsetCandidateCode (arity threshold : ℕ) : DecidableEq ↥(CandidateCode arity threshold)

Equations

• Complexity.AntiChecker.instDecidableEqSubtypeListBoolMemFinsetCandidateCode arity threshold = Complexity.AntiChecker.instDecidableEqSubtypeListBoolMemFinsetCandidateCode._aux_1 arity threshold