Good-string binomial-tail bound -- proof internals

theorem Complexity.AntiChecker.card_caughtSurvivorTuples_le_upperBound_internal {arity : ℕ} (target : BitString arity → Bool) (threshold : ℕ) (inputs : List (BitString arity)) (input : BitString arity) : (caughtSurvivorTuples target threshold inputs input).card ≤ caughtTupleUpperBound arity (candidateSurvivorCount target threshold inputs) (disagreeingSurvivors target threshold inputs input).card

theorem Complexity.AntiChecker.exists_input_survivorCount_le_sixteen_mul_disagreements_internal {arity : ℕ} (harity : 0 < arity) (target : BitString arity → Bool) (threshold : ℕ) (inputs : List (BitString arity)) (hall : EverySurvivorTupleCaught target threshold inputs) : ∃ (input : BitString arity), candidateSurvivorCount target threshold inputs ≤ 16 * (disagreeingSurvivors target threshold inputs input).card

theorem Complexity.AntiChecker.hasShrinkExtension_two_mul_arity_internal {arity : ℕ} (harity : 8 ≤ arity) (target : BitString arity → Bool) (threshold : ℕ) (inputs : List (BitString arity)) (hall : EverySurvivorTupleCaught target threshold inputs) : HasShrinkExtension (2 * arity) target threshold inputs