Finite circuit-code enumeration

This module supplies a canonical finite domain for anti-checker survivor counts. It enumerates all bit strings within the circuit-code length bound and filters them to well-formed circuits within a size threshold. The resulting set covers every small typed circuit, has an explicit cardinality bound, and turns worst-case circuit hardness into the pointwise-failure premise needed by finite anti-checker extraction.

This exhaustive bound is a baseline, not the quantitative Anti-Checker Lemma: the later approximate-counting argument must compress the extracted sample list to the lemma's much smaller target length.

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

Exact-length code enumeration contains precisely the lists of that length.

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

There are exactly 2 ^ length Boolean codes of a fixed length.

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

Bounded-length code enumeration contains precisely the lists within the bound.

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

The number of Boolean codes up to a length bound is at most the next power of two.

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

Candidate membership splits into the code-length bound and decoded small-circuit validity.

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

The canonical candidate circuit-code domain has an explicit exponential cardinality bound.

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

Every typed circuit within the size threshold has its canonical encoding in the candidate domain.

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

If the target has no circuit within the threshold, every canonical candidate code disagrees with it somewhere.

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

Exhaustive finite extraction gives an anti-checker no longer than the canonical candidate-code domain.

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

Fully numerical exhaustive bound for finite anti-checker extraction.