Anti-checker shrink rounds

One shrink round bounds the next survivor count by a fixed fraction of the current count. This module composes a trace of such rounds into an exact natural-number power inequality. If that upper bound is smaller than one after rescaling, the final survivor count is zero and the trace is an anti-checker. The halving submodule gives a convenient blockwise stopping rule, and the selection submodule constructs traces by approximate minimization.

@[simp]

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

The empty list is a valid shrink trace.

@[simp]

theorem Complexity.AntiChecker.isShrinkTrace_cons_iff {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

Consing an input extends a shrink trace exactly when it shrinks the prefix represented by the tail.

theorem Complexity.AntiChecker.IsShrinkTrace.scaledCandidateSurvivorCount {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 []

Composing every round in a shrink trace gives the exact scaled survivor bound with one factor per selected input.

theorem Complexity.AntiChecker.IsShrinkTrace.candidateSurvivorCount_eq_zero {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

If the composed upper bound is smaller than one after rescaling, no canonical candidate survives the trace.

theorem Complexity.AntiChecker.IsShrinkTrace.isFor {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

A shrink trace whose composed bound is below one is an anti-checker.