Anti-checker survivor counts

The constructive Anti-Checker Lemma builds a sample prefix while estimating the number of encoded small circuits still consistent with its target labels. This module exposes that exact finite count, its monotonicity under adding samples, and its specialization to the canonical bounded circuit enumeration.

For canonical candidates, reaching zero survivors is exactly the anti-checker condition. Approximate counters can therefore target this quantity without any gap between encoded-circuit and typed-circuit semantics.

theorem Complexity.AntiChecker.survivorCount_nil {arity : ℕ} (target : BitString arity → Bool) (codes : Finset (List Bool)) : survivorCount target [] codes = codes.card

Before any samples are chosen, every candidate code survives.

theorem Complexity.AntiChecker.survivorCount_cons {arity : ℕ} (target : BitString arity → Bool) (input : BitString arity) (inputs : List (BitString arity)) (codes : Finset (List Bool)) : survivorCount target (input :: inputs) codes = {x ∈ ConsistentCodes target inputs codes | CodeAgreesAt target x input}.card

Adding one input counts the previous survivors that agree with its target label.

theorem Complexity.AntiChecker.survivorCount_le_card {arity : ℕ} (target : BitString arity → Bool) (inputs : List (BitString arity)) (codes : Finset (List Bool)) : survivorCount target inputs codes ≤ codes.card

A survivor count never exceeds the original candidate-set size.

theorem Complexity.AntiChecker.survivorCount_samples_anti {arity : ℕ} {target : BitString arity → Bool} {first second : List (BitString arity)} {codes : Finset (List Bool)} (hsub : ∀ input ∈ first, input ∈ second) : survivorCount target second codes ≤ survivorCount target first codes

Adding possible samples can only decrease the survivor count.

theorem Complexity.AntiChecker.survivorCount_eq_zero_iff {arity : ℕ} (target : BitString arity → Bool) (inputs : List (BitString arity)) (codes : Finset (List Bool)) : survivorCount target inputs codes = 0 ↔ ConsistentCodes target inputs codes = ∅

A survivor count is zero exactly when its survivor set is empty.

theorem Complexity.AntiChecker.candidateSurvivorCount_nil {arity threshold : ℕ} (target : BitString arity → Bool) : candidateSurvivorCount target threshold [] = (candidateCodes arity threshold).card

The initial canonical survivor count is the size of the bounded circuit enumeration.

theorem Complexity.AntiChecker.candidateSurvivorCount_cons {arity threshold : ℕ} (target : BitString arity → Bool) (input : BitString arity) (inputs : List (BitString arity)) : candidateSurvivorCount target threshold (input :: inputs) = {x ∈ ConsistentCodes target inputs (candidateCodes arity threshold) | CodeAgreesAt target x input}.card

Adding one input to the canonical sample prefix filters precisely the previous canonical survivors.

theorem Complexity.AntiChecker.candidateSurvivorCount_le_card {arity threshold : ℕ} (target : BitString arity → Bool) (inputs : List (BitString arity)) : candidateSurvivorCount target threshold inputs ≤ (candidateCodes arity threshold).card

Canonical survivors are bounded by the canonical candidate domain.

theorem Complexity.AntiChecker.candidateSurvivorCount_samples_anti {arity threshold : ℕ} {target : BitString arity → Bool} {first second : List (BitString arity)} (hsub : ∀ input ∈ first, input ∈ second) : candidateSurvivorCount target threshold second ≤ candidateSurvivorCount target threshold first

Adding possible samples can only decrease the canonical survivor count.

theorem Complexity.AntiChecker.candidateSurvivorCount_eq_zero_iff_isFor {arity threshold : ℕ} [NeZero arity] (target : BitString arity → Bool) (inputs : List (BitString arity)) : candidateSurvivorCount target threshold inputs = 0 ↔ IsFor target threshold inputs

For the canonical candidate domain, zero survivors is exactly the typed anti-checker condition.