Anti-checker survivor counts -- definitions

This layer names the exact finite count estimated in the constructive Anti-Checker Lemma: the number of candidate circuit descriptions consistent with all target-labelled inputs chosen so far.

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

Number of codes from a finite domain that remain consistent with all sampled target values.

Equations

• Complexity.AntiChecker.survivorCount target inputs codes = (Complexity.AntiChecker.ConsistentCodes target inputs codes).card

def Complexity.AntiChecker.candidateSurvivorCount {arity : ℕ} (target : BitString arity → Bool) (threshold : ℕ) (inputs : List (BitString arity)) : ℕ

Survivor count specialized to the canonical enumeration of circuits within a size threshold.

Equations

• Complexity.AntiChecker.candidateSurvivorCount target threshold inputs = Complexity.AntiChecker.survivorCount target inputs (Complexity.AntiChecker.candidateCodes arity threshold)