Good-string combinatorics -- proof internals

theorem Complexity.AntiChecker.survivorCodeOutput_eq_target_iff_internal {arity : ℕ} (target : BitString arity → Bool) (threshold : ℕ) (inputs : List (BitString arity)) (code : ↥(SurvivorCode target threshold inputs)) (input : BitString arity) : survivorCodeOutput target threshold inputs code input = target input ↔ CodeAgreesAt target (↑code) input

theorem Complexity.AntiChecker.card_survivorCode_internal {arity : ℕ} (target : BitString arity → Bool) (threshold : ℕ) (inputs : List (BitString arity)) : Fintype.card ↥(SurvivorCode target threshold inputs) = candidateSurvivorCount target threshold inputs

theorem Complexity.AntiChecker.isSurvivorTupleCaughtAt_iff_agreementCount_le_internal {arity : ℕ} (target : BitString arity → Bool) (threshold : ℕ) (inputs : List (BitString arity)) (input : BitString arity) (tuple : Fin arity → ↥(SurvivorCode target threshold inputs)) : IsSurvivorTupleCaughtAt target threshold inputs input tuple ↔ survivorTupleAgreementCount target threshold inputs input tuple ≤ arity / 2

theorem Complexity.AntiChecker.survivorTupleMajority_eq_target_of_not_caught_internal {arity : ℕ} (target : BitString arity → Bool) (threshold : ℕ) (inputs : List (BitString arity)) (input : BitString arity) (tuple : Fin arity → ↥(SurvivorCode target threshold inputs)) (hnotCaught : ¬IsSurvivorTupleCaughtAt target threshold inputs input tuple) : (majority fun (i : Fin arity) => survivorCodeOutput target threshold inputs (tuple i) input) = target input

theorem Complexity.AntiChecker.everySurvivorTupleCaught_of_no_majorityComputes_internal {arity : ℕ} (target : BitString arity → Bool) (threshold : ℕ) (inputs : List (BitString arity)) (hnoMajority : ∀ (tuple : Fin arity → ↥(SurvivorCode target threshold inputs)), ¬SurvivorTupleMajorityComputes target threshold inputs tuple) : EverySurvivorTupleCaught target threshold inputs

theorem Complexity.AntiChecker.card_caughtSurvivorTuples_internal {arity : ℕ} (target : BitString arity → Bool) (threshold : ℕ) (inputs : List (BitString arity)) (input : BitString arity) : (caughtSurvivorTuples target threshold inputs input).card = ∑ disagreements ∈ Finset.Icc (arity - arity / 2) arity, arity.choose disagreements * (disagreeingSurvivors target threshold inputs input).card ^ disagreements * (candidateSurvivorCount target threshold inputs - (disagreeingSurvivors target threshold inputs input).card) ^ (arity - disagreements)

theorem Complexity.AntiChecker.card_disagreeingSurvivors_add_next_internal {arity : ℕ} (target : BitString arity → Bool) (threshold : ℕ) (inputs : List (BitString arity)) (input : BitString arity) : (disagreeingSurvivors target threshold inputs input).card + candidateSurvivorCount target threshold (input :: inputs) = candidateSurvivorCount target threshold inputs

theorem Complexity.AntiChecker.isShrinkExtension_iff_survivorCount_le_mul_disagreements_internal {arity denominator threshold : ℕ} (hdenominator : 0 < denominator) (target : BitString arity → Bool) (inputs : List (BitString arity)) (input : BitString arity) : IsShrinkExtension denominator target threshold inputs input ↔ candidateSurvivorCount target threshold inputs ≤ denominator * (disagreeingSurvivors target threshold inputs input).card

theorem Complexity.AntiChecker.exists_input_many_caughtSurvivorTuples_internal {arity : ℕ} (target : BitString arity → Bool) (threshold : ℕ) (inputs : List (BitString arity)) (hall : EverySurvivorTupleCaught target threshold inputs) : ∃ (input : BitString arity), candidateSurvivorCount target threshold inputs ^ arity ≤ 2 ^ arity * (caughtSurvivorTuples target threshold inputs input).card