Finite anti-checker extraction -- proof internals

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

theorem Complexity.AntiChecker.mem_consistentCodes_iff_internal {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

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

theorem Complexity.AntiChecker.consistentCodes_cons_internal {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}

theorem Complexity.AntiChecker.consistentCodes_samples_anti_internal {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

theorem Complexity.AntiChecker.exists_inputs_consistentCodes_eq_empty_internal {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 = ∅

theorem Complexity.AntiChecker.isFor_of_consistentCodes_eq_empty_internal {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

theorem Complexity.AntiChecker.exists_isFor_length_le_card_internal {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

theorem Complexity.AntiChecker.exists_encode_not_mem_length_le_card_internal {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