Finite anti-checkers -- proof internals

theorem Complexity.AntiChecker.isFor_iff_forall_not_agreesOn_internal {arity : ℕ} [NeZero arity] (target : BitString arity → Bool) (threshold : ℕ) (inputs : List (BitString arity)) : IsFor target threshold inputs ↔ ∀ (internalGates : ℕ) (circuit : Circuit Basis.andOr2 arity 1 internalGates), circuit.size ≤ threshold → ¬AgreesOn circuit target inputs

theorem Complexity.AntiChecker.isFor_inputs_mono_internal {arity : ℕ} [NeZero arity] {target : BitString arity → Bool} {threshold : ℕ} {first second : List (BitString arity)} (hsub : ∀ input ∈ first, input ∈ second) (hanti : IsFor target threshold first) : IsFor target threshold second

theorem Complexity.AntiChecker.isFor_threshold_anti_internal {arity : ℕ} [NeZero arity] {target : BitString arity → Bool} {first second : ℕ} {inputs : List (BitString arity)} (hthreshold : first ≤ second) (hanti : IsFor target second inputs) : IsFor target first inputs

theorem Complexity.AntiChecker.isFor_perm_internal {arity : ℕ} [NeZero arity] {target : BitString arity → Bool} {threshold : ℕ} {first second : List (BitString arity)} (hperm : first.Perm second) : IsFor target threshold first ↔ IsFor target threshold second

theorem Complexity.AntiChecker.length_padInputsTo_internal {arity targetLength : ℕ} {inputs : List (BitString arity)} (hlength : inputs.length ≤ targetLength) : (padInputsTo targetLength inputs).length = targetLength

theorem Complexity.AntiChecker.mem_padInputsTo_of_mem_internal {arity targetLength : ℕ} {inputs : List (BitString arity)} {input : BitString arity} (hinput : input ∈ inputs) : input ∈ padInputsTo targetLength inputs

theorem Complexity.AntiChecker.IsFor.padInputsTo_internal {arity threshold targetLength : ℕ} [NeZero arity] {target : BitString arity → Bool} {inputs : List (BitString arity)} (hanti : IsFor target threshold inputs) : IsFor target threshold (padInputsTo targetLength inputs)

theorem Complexity.AntiChecker.samplesFunction_ofInputs_iff_agreesOn_internal {arity threshold : ℕ} [NeZero arity] (target : BitString arity → Bool) (inputs : List (BitString arity)) {internalGates : ℕ} (circuit : Circuit Basis.andOr2 arity 1 internalGates) : ((SuccinctMCSP.Instance.ofInputs threshold target inputs).SamplesFunction fun (input : BitString (SuccinctMCSP.Instance.ofInputs threshold target inputs).arity) => circuit.eval input 0) ↔ AgreesOn circuit target inputs

theorem Complexity.AntiChecker.isFor_iff_not_hasCircuitAtMost_internal {arity threshold : ℕ} [NeZero arity] (target : BitString arity → Bool) (inputs : List (BitString arity)) : IsFor target threshold inputs ↔ ¬(SuccinctMCSP.Instance.ofInputs threshold target inputs).HasCircuitAtMost

theorem Complexity.AntiChecker.encode_not_mem_iff_isFor_internal {arity threshold : ℕ} [NeZero arity] (target : BitString arity → Bool) (inputs : List (BitString arity)) : (SuccinctMCSP.Instance.ofInputs threshold target inputs).encode ∉ SuccinctMCSP ↔ IsFor target threshold inputs