Finite anti-checker extraction -- definitions

This layer tracks a finite set of machine-facing circuit descriptions that are still consistent with all sampled target values. It is deliberately generic in the initial code set: later enumeration or approximate-counting arguments can supply the candidates and prove that they cover every small typed circuit.

def Complexity.AntiChecker.CodeAgreesAt {arity : ℕ} (target : BitString arity → Bool) (code : List Bool) (input : BitString arity) : Prop

One encoded circuit agrees with the target at one typed input. Malformed or non-evaluating codes do not agree.

Equations

• Complexity.AntiChecker.CodeAgreesAt target code input = (Complexity.CircuitCode.evalCode arity code input.toList = some (target input))

@[instance_reducible]

instance Complexity.AntiChecker.instDecidableCodeAgreesAt {arity : ℕ} (target : BitString arity → Bool) (code : List Bool) (input : BitString arity) : Decidable (CodeAgreesAt target code input)

Equations

• Complexity.AntiChecker.instDecidableCodeAgreesAt target code input = id inferInstance

def Complexity.AntiChecker.ConsistentCode {arity : ℕ} (target : BitString arity → Bool) (inputs : List (BitString arity)) (code : List Bool) : Prop

A code is consistent with every target-labelled input in the list.

Equations

• Complexity.AntiChecker.ConsistentCode target inputs code = List.Forall (Complexity.AntiChecker.CodeAgreesAt target code) inputs

@[instance_reducible]

instance Complexity.AntiChecker.instDecidableConsistentCode {arity : ℕ} (target : BitString arity → Bool) (inputs : List (BitString arity)) (code : List Bool) : Decidable (ConsistentCode target inputs code)

Equations

• Complexity.AntiChecker.instDecidableConsistentCode target inputs code = id inferInstance

def Complexity.AntiChecker.ConsistentCodes {arity : ℕ} (target : BitString arity → Bool) (inputs : List (BitString arity)) (codes : Finset (List Bool)) : Finset (List Bool)

Candidate circuit codes surviving every sampled target value.

Equations

• Complexity.AntiChecker.ConsistentCodes target inputs codes = Finset.filter (Complexity.AntiChecker.ConsistentCode target inputs) codes

def Complexity.AntiChecker.CoversThreshold {arity : ℕ} [NeZero arity] (threshold : ℕ) (codes : Finset (List Bool)) : Prop

The finite code set contains the canonical encoding of every typed circuit within the size threshold.

Equations

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

def Complexity.AntiChecker.AllFailSomewhere {arity : ℕ} (target : BitString arity → Bool) (codes : Finset (List Bool)) : Prop

Every candidate code disagrees with the target on some input.

Equations

• Complexity.AntiChecker.AllFailSomewhere target codes = ∀ code ∈ codes, ∃ (input : Complexity.BitString arity), ¬Complexity.AntiChecker.CodeAgreesAt target code input