Approximate-selection round traces -- proof internals #
theorem
Complexity.AntiChecker.ApproximatesEveryRound.approximatesRoundsUpTo_internal
{arity precision threshold : ℕ}
{target : BitString arity → Bool}
{estimator : List (BitString arity) → BitString arity → ℕ}
(happrox : ApproximatesEveryRound precision target threshold estimator)
(rounds : ℕ)
:
ApproximatesRoundsUpTo rounds precision target threshold estimator
theorem
Complexity.AntiChecker.isEstimateSelectionTrace_nil_internal
{arity : ℕ}
(estimator : List (BitString arity) → BitString arity → ℕ)
:
IsEstimateSelectionTrace estimator []
theorem
Complexity.AntiChecker.isEstimateSelectionTrace_cons_iff_internal
{arity : ℕ}
(estimator : List (BitString arity) → BitString arity → ℕ)
(input : BitString arity)
(inputs : List (BitString arity))
:
IsEstimateSelectionTrace estimator (input :: inputs) ↔ IsEstimateSelectionTrace estimator inputs ∧ IsEstimateMinimizer (estimator inputs) input
theorem
Complexity.AntiChecker.IsEstimateSelectionTrace.isShrinkTrace_internal
{arity precision denominator threshold : ℕ}
{target : BitString arity → Bool}
{estimator : List (BitString arity) → BitString arity → ℕ}
{inputs : List (BitString arity)}
(hprecision : 1 < precision)
(hdenominator : 0 < denominator)
(hbound : 4 * denominator ≤ precision + 3)
(happrox : ApproximatesEveryRound precision target threshold estimator)
(hgood : ∀ (samplePrefix : List (BitString arity)), HasShrinkExtension denominator target threshold samplePrefix)
(htrace : IsEstimateSelectionTrace estimator inputs)
:
IsShrinkTrace (2 * denominator) target threshold inputs
theorem
Complexity.AntiChecker.IsEstimateSelectionTrace.isShrinkTrace_of_length_le_internal
{arity rounds precision denominator threshold : ℕ}
{target : BitString arity → Bool}
{estimator : List (BitString arity) → BitString arity → ℕ}
{inputs : List (BitString arity)}
(hprecision : 1 < precision)
(hdenominator : 0 < denominator)
(hbound : 4 * denominator ≤ precision + 3)
(happrox : ApproximatesRoundsUpTo rounds precision target threshold estimator)
(hgood : ∀ (samplePrefix : List (BitString arity)), HasShrinkExtension denominator target threshold samplePrefix)
(htrace : IsEstimateSelectionTrace estimator inputs)
(hlength : inputs.length ≤ rounds)
:
IsShrinkTrace (2 * denominator) target threshold inputs
theorem
Complexity.AntiChecker.exists_isShrinkTrace_length_of_approximatesEveryRound_internal
{arity precision denominator threshold : ℕ}
{target : BitString arity → Bool}
(estimator : List (BitString arity) → BitString arity → ℕ)
(rounds : ℕ)
(hprecision : 1 < precision)
(hdenominator : 0 < denominator)
(hbound : 4 * denominator ≤ precision + 3)
(happrox : ApproximatesEveryRound precision target threshold estimator)
(hgood : ∀ (samplePrefix : List (BitString arity)), HasShrinkExtension denominator target threshold samplePrefix)
:
theorem
Complexity.AntiChecker.exists_isShrinkTrace_length_of_approximatesRoundsUpTo_internal
{arity precision denominator threshold : ℕ}
{target : BitString arity → Bool}
(estimator : List (BitString arity) → BitString arity → ℕ)
(rounds : ℕ)
(hprecision : 1 < precision)
(hdenominator : 0 < denominator)
(hbound : 4 * denominator ≤ precision + 3)
(happrox : ApproximatesRoundsUpTo rounds precision target threshold estimator)
(hgood : ∀ (samplePrefix : List (BitString arity)), HasShrinkExtension denominator target threshold samplePrefix)
: