Halving bounds for anti-checker shrink rounds -- proof internals

theorem Complexity.AntiChecker.two_mul_sub_one_pow_le_pow_internal {denominator : ℕ} (hdenominator : 2 ≤ denominator) : 2 * (denominator - 1) ^ denominator ≤ denominator ^ denominator

theorem Complexity.AntiChecker.two_pow_mul_sub_one_pow_mul_le_pow_mul_internal {denominator : ℕ} (hdenominator : 2 ≤ denominator) (blocks : ℕ) : 2 ^ blocks * (denominator - 1) ^ (denominator * blocks) ≤ denominator ^ (denominator * blocks)

theorem Complexity.AntiChecker.IsShrinkTrace.candidateSurvivorCount_eq_zero_of_initial_lt_two_pow_internal {arity denominator threshold blocks : ℕ} {target : BitString arity → Bool} {inputs : List (BitString arity)} (htrace : IsShrinkTrace denominator target threshold inputs) (hdenominator : 2 ≤ denominator) (hlength : inputs.length = denominator * blocks) (hinitial : candidateSurvivorCount target threshold [] < 2 ^ blocks) : candidateSurvivorCount target threshold inputs = 0

theorem Complexity.AntiChecker.IsShrinkTrace.isFor_of_initial_lt_two_pow_internal {arity denominator threshold blocks : ℕ} [NeZero arity] {target : BitString arity → Bool} {inputs : List (BitString arity)} (htrace : IsShrinkTrace denominator target threshold inputs) (hdenominator : 2 ≤ denominator) (hlength : inputs.length = denominator * blocks) (hinitial : candidateSurvivorCount target threshold [] < 2 ^ blocks) : IsFor target threshold inputs