Finite circuit-code enumeration -- proof internals

theorem Complexity.AntiChecker.mem_codesOfLength_iff_internal {length : ℕ} {code : List Bool} : code ∈ codesOfLength length ↔ code.length = length

theorem Complexity.AntiChecker.card_codesOfLength_internal (length : ℕ) : (codesOfLength length).card = 2 ^ length

theorem Complexity.AntiChecker.mem_codesUpTo_iff_internal {bound : ℕ} {code : List Bool} : code ∈ codesUpTo bound ↔ code.length ≤ bound

theorem Complexity.AntiChecker.card_codesUpTo_le_internal (bound : ℕ) : (codesUpTo bound).card ≤ 2 ^ (bound + 1)

theorem Complexity.AntiChecker.mem_candidateCodes_iff_internal {arity threshold : ℕ} {code : List Bool} : code ∈ candidateCodes arity threshold ↔ code.length ≤ codeLengthBound arity threshold ∧ IsSmallCircuitCode arity threshold code

theorem Complexity.AntiChecker.card_candidateCodes_le_internal (arity threshold : ℕ) : (candidateCodes arity threshold).card ≤ 2 ^ (codeLengthBound arity threshold + 1)

theorem Complexity.AntiChecker.candidateCodes_coversThreshold_internal (arity threshold : ℕ) [NeZero arity] : CoversThreshold threshold (candidateCodes arity threshold)

theorem Complexity.AntiChecker.candidateCodes_allFailSomewhere_internal {arity threshold : ℕ} [NeZero arity] (target : BitString arity → Bool) (hhard : ¬(MCSP.Instance.ofFunction arity threshold target).HasCircuitAtMost) : AllFailSomewhere target (candidateCodes arity threshold)

theorem Complexity.AntiChecker.exists_isFor_length_le_candidateCard_internal {arity threshold : ℕ} [NeZero arity] (target : BitString arity → Bool) (hhard : ¬(MCSP.Instance.ofFunction arity threshold target).HasCircuitAtMost) : ∃ (inputs : List (BitString arity)), inputs.length ≤ (candidateCodes arity threshold).card ∧ IsFor target threshold inputs

theorem Complexity.AntiChecker.exists_isFor_length_le_codeBound_internal {arity threshold : ℕ} [NeZero arity] (target : BitString arity → Bool) (hhard : ¬(MCSP.Instance.ofFunction arity threshold target).HasCircuitAtMost) : ∃ (inputs : List (BitString arity)), inputs.length ≤ 2 ^ (codeLengthBound arity threshold + 1) ∧ IsFor target threshold inputs