Finite anti-checker extraction

This module exposes the finite survivor-set argument behind anti-checker extraction. Starting from a finite set of circuit codes, one records the codes consistent with all samples chosen so far. If every original code fails on some input, at most one chosen failure input per code empties the survivor set. If the original codes cover all circuits below a threshold, the resulting input list is an anti-checker and its canonical SuccinctMCSP instance rejects.

The construction is intentionally conditional on a finite covering code set. Building and bounding that set is a separate quantitative step.

theorem Complexity.AntiChecker.consistentCode_iff_forall_mem {arity : ℕ} (target : BitString arity → Bool) (inputs : List (BitString arity)) (code : List Bool) : ConsistentCode target inputs code ↔ ∀ input ∈ inputs, CodeAgreesAt target code input

List consistency is pointwise agreement at every member.

theorem Complexity.AntiChecker.mem_consistentCodes_iff {arity : ℕ} (target : BitString arity → Bool) (inputs : List (BitString arity)) (codes : Finset (List Bool)) (code : List Bool) : code ∈ ConsistentCodes target inputs codes ↔ code ∈ codes ∧ ConsistentCode target inputs code

Membership in the survivor set splits into original membership and sample consistency.

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

With no samples, every original candidate survives.

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

Adding one sample filters the previous survivor set by agreement there.

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

Adding samples can only remove surviving candidate codes.

theorem Complexity.AntiChecker.exists_inputs_consistentCodes_eq_empty {arity : ℕ} (target : BitString arity → Bool) (codes : Finset (List Bool)) (hfail : AllFailSomewhere target codes) : ∃ (inputs : List (BitString arity)), inputs.length ≤ codes.card ∧ ConsistentCodes target inputs codes = ∅

If every finite candidate fails somewhere, at most one failure input per candidate empties the survivor set.

theorem Complexity.AntiChecker.IsFor.of_consistentCodes_eq_empty {arity threshold : ℕ} [NeZero arity] (target : BitString arity → Bool) (inputs : List (BitString arity)) (codes : Finset (List Bool)) (hcovers : CoversThreshold threshold codes) (hempty : ConsistentCodes target inputs codes = ∅) : IsFor target threshold inputs

Emptying a code set that covers every small typed circuit produces an anti-checker for the target.

theorem Complexity.AntiChecker.exists_isFor_length_le_card {arity threshold : ℕ} [NeZero arity] (target : BitString arity → Bool) (codes : Finset (List Bool)) (hcovers : CoversThreshold threshold codes) (hfail : AllFailSomewhere target codes) : ∃ (inputs : List (BitString arity)), inputs.length ≤ codes.card ∧ IsFor target threshold inputs

Finite extraction theorem: a covering set whose candidates all fail yields an anti-checker no longer than the candidate set.

theorem Complexity.AntiChecker.exists_encode_not_mem_length_le_card {arity threshold : ℕ} [NeZero arity] (target : BitString arity → Bool) (codes : Finset (List Bool)) (hcovers : CoversThreshold threshold codes) (hfail : AllFailSomewhere target codes) : ∃ (inputs : List (BitString arity)), inputs.length ≤ codes.card ∧ (SuccinctMCSP.Instance.ofInputs threshold target inputs).encode ∉ SuccinctMCSP

The canonical SuccinctMCSP instance induced by the extracted anti-checker is a no-instance.