Anti-checker survivor counts -- proof internals

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

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

theorem Complexity.AntiChecker.survivorCount_le_card_internal {arity : ℕ} (target : BitString arity → Bool) (inputs : List (BitString arity)) (codes : Finset (List Bool)) : survivorCount target inputs codes ≤ codes.card

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

theorem Complexity.AntiChecker.survivorCount_eq_zero_iff_internal {arity : ℕ} (target : BitString arity → Bool) (inputs : List (BitString arity)) (codes : Finset (List Bool)) : survivorCount target inputs codes = 0 ↔ ConsistentCodes target inputs codes = ∅

theorem Complexity.AntiChecker.candidateSurvivorCount_nil_internal {arity threshold : ℕ} (target : BitString arity → Bool) : candidateSurvivorCount target threshold [] = (candidateCodes arity threshold).card

theorem Complexity.AntiChecker.candidateSurvivorCount_cons_internal {arity threshold : ℕ} (target : BitString arity → Bool) (input : BitString arity) (inputs : List (BitString arity)) : candidateSurvivorCount target threshold (input :: inputs) = {x ∈ ConsistentCodes target inputs (candidateCodes arity threshold) | CodeAgreesAt target x input}.card

theorem Complexity.AntiChecker.candidateSurvivorCount_le_card_internal {arity threshold : ℕ} (target : BitString arity → Bool) (inputs : List (BitString arity)) : candidateSurvivorCount target threshold inputs ≤ (candidateCodes arity threshold).card

theorem Complexity.AntiChecker.candidateSurvivorCount_samples_anti_internal {arity threshold : ℕ} {target : BitString arity → Bool} {first second : List (BitString arity)} (hsub : ∀ input ∈ first, input ∈ second) : candidateSurvivorCount target threshold second ≤ candidateSurvivorCount target threshold first

theorem Complexity.AntiChecker.candidateSurvivorCount_eq_zero_iff_isFor_internal {arity threshold : ℕ} [NeZero arity] (target : BitString arity → Bool) (inputs : List (BitString arity)) : candidateSurvivorCount target threshold inputs = 0 ↔ IsFor target threshold inputs