Approximate-count selection

This module formalizes one selection round in the constructive Anti-Checker Lemma. A minimum estimated extension exists because the input domain is finite. If all estimates satisfy the relative-count contract, minimizing them transfers a genuinely good input's survivor-count shrinkage to the chosen input.

The quantitative theorem is exact over natural numbers: when the relative precision p and shrink denominator d satisfy 4 * d ≤ p + 3, an existing 1 / d shrink gives the approximate minimizer a 1 / (2 * d) shrink. At the paper's parameters this is the passage from 1 / (2n) to 1 / (4n).

theorem Complexity.AntiChecker.exists_isEstimateMinimizer {arity : ℕ} (estimate : BitString arity → ℕ) : ∃ (chosen : BitString arity), IsEstimateMinimizer estimate chosen

A minimum natural-valued estimate exists over the finite Boolean input domain.

theorem Complexity.AntiChecker.IsEstimateMinimizer.candidateSurvivorCount_le_scaled {arity precision threshold : ℕ} {target : BitString arity → Bool} {inputs : List (BitString arity)} {estimate : BitString arity → ℕ} {chosen other : BitString arity} (happrox : ApproximatesAllExtensions precision target threshold inputs estimate) (hminimum : IsEstimateMinimizer estimate chosen) : (precision - 1) * candidateSurvivorCount target threshold (chosen :: inputs) ≤ (precision + 1) * candidateSurvivorCount target threshold (other :: inputs)

An approximate minimizer's true extension count is bounded by any other extension's count, up to the relative-error factors.

theorem Complexity.AntiChecker.IsEstimateMinimizer.scaledShrink_of_hasShrinkExtension {arity precision denominator threshold : ℕ} {target : BitString arity → Bool} {inputs : List (BitString arity)} {estimate : BitString arity → ℕ} {chosen : BitString arity} (happrox : ApproximatesAllExtensions precision target threshold inputs estimate) (hminimum : IsEstimateMinimizer estimate chosen) (hgood : HasShrinkExtension denominator target threshold inputs) : denominator * (precision - 1) * candidateSurvivorCount target threshold (chosen :: inputs) ≤ (precision + 1) * (denominator - 1) * candidateSurvivorCount target threshold inputs

If some extension shrinks by 1 / denominator, approximate minimization gives the following exact scaled survivor-count bound.

theorem Complexity.AntiChecker.relativeApproximation_coefficient_le {precision denominator : ℕ} (hprecision : 1 < precision) (hdenominator : 0 < denominator) (hbound : 4 * denominator ≤ precision + 3) : 2 * (precision + 1) * (denominator - 1) ≤ (precision - 1) * (2 * denominator - 1)

The arithmetic condition that makes relative error consume at most half of the available shrinkage.

theorem Complexity.AntiChecker.IsEstimateMinimizer.isShrinkExtension_double {arity precision denominator threshold : ℕ} {target : BitString arity → Bool} {inputs : List (BitString arity)} {estimate : BitString arity → ℕ} {chosen : BitString arity} (hprecision : 1 < precision) (hdenominator : 0 < denominator) (hbound : 4 * denominator ≤ precision + 3) (happrox : ApproximatesAllExtensions precision target threshold inputs estimate) (hminimum : IsEstimateMinimizer estimate chosen) (hgood : HasShrinkExtension denominator target threshold inputs) : IsShrinkExtension (2 * denominator) target threshold inputs chosen

A minimum relative estimate inherits an existing 1 / denominator shrink as a 1 / (2 * denominator) shrink.