Approximate-count selection -- definitions

This layer describes one round of the constructive anti-checker procedure. It chooses an input minimizing the estimated survivor count and records shrinkage using cross-multiplied natural inequalities.

def Complexity.AntiChecker.IsEstimateMinimizer {arity : ℕ} (estimate : BitString arity → ℕ) (chosen : BitString arity) : Prop

An input minimizes a natural-valued estimate over all inputs of the fixed arity.

Equations

• Complexity.AntiChecker.IsEstimateMinimizer estimate chosen = ∀ (input : Complexity.BitString arity), estimate chosen ≤ estimate input

def Complexity.AntiChecker.ApproximatesAllExtensions {arity : ℕ} (precision : ℕ) (target : BitString arity → Bool) (threshold : ℕ) (inputs : List (BitString arity)) (estimate : BitString arity → ℕ) : Prop

Estimates for every possible one-input extension satisfy the relative survivor-count contract.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.AntiChecker.IsShrinkExtension {arity : ℕ} (denominator : ℕ) (target : BitString arity → Bool) (threshold : ℕ) (inputs : List (BitString arity)) (input : BitString arity) : Prop

Adding input reduces the canonical survivor count by at least the fraction 1 / denominator, represented without division.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.AntiChecker.HasShrinkExtension {arity : ℕ} (denominator : ℕ) (target : BitString arity → Bool) (threshold : ℕ) (inputs : List (BitString arity)) : Prop

Some one-input extension reduces the canonical survivor count by the requested fraction.

Equations

• One or more equations did not get rendered due to their size.