Anti-checker shrink rounds -- proof internals

theorem Complexity.AntiChecker.isShrinkTrace_nil_internal {arity denominator threshold : ℕ} (target : BitString arity → Bool) : IsShrinkTrace denominator target threshold []

theorem Complexity.AntiChecker.isShrinkTrace_cons_iff_internal {arity denominator threshold : ℕ} (target : BitString arity → Bool) (input : BitString arity) (inputs : List (BitString arity)) : IsShrinkTrace denominator target threshold (input :: inputs) ↔ IsShrinkTrace denominator target threshold inputs ∧ IsShrinkExtension denominator target threshold inputs input

theorem Complexity.AntiChecker.IsShrinkTrace.scaledCandidateSurvivorCount_internal {arity denominator threshold : ℕ} {target : BitString arity → Bool} {inputs : List (BitString arity)} (htrace : IsShrinkTrace denominator target threshold inputs) : denominator ^ inputs.length * candidateSurvivorCount target threshold inputs ≤ (denominator - 1) ^ inputs.length * candidateSurvivorCount target threshold []

theorem Complexity.AntiChecker.IsShrinkTrace.candidateSurvivorCount_eq_zero_internal {arity denominator threshold : ℕ} {target : BitString arity → Bool} {inputs : List (BitString arity)} (htrace : IsShrinkTrace denominator target threshold inputs) (hbound : (denominator - 1) ^ inputs.length * candidateSurvivorCount target threshold [] < denominator ^ inputs.length) : candidateSurvivorCount target threshold inputs = 0

theorem Complexity.AntiChecker.IsShrinkTrace.isFor_internal {arity denominator threshold : ℕ} [NeZero arity] {target : BitString arity → Bool} {inputs : List (BitString arity)} (htrace : IsShrinkTrace denominator target threshold inputs) (hbound : (denominator - 1) ^ inputs.length * candidateSurvivorCount target threshold [] < denominator ^ inputs.length) : IsFor target threshold inputs