Uniform good seeds for bounded-error machines

This module specializes the finite probabilistic method to bounded-error machines. After 12 * (n + 1) + 1 independent trials, one compact random seed gives the correct majority verdict simultaneously on every n-bit input.

The result only concerns the fixed-time acceptance event, so it does not need an all-paths-halting hypothesis.

def Complexity.NTM.uniformSeedRuns (n : ℕ) : ℕ

Number of independent trials used to select one seed that is correct on every input of length n. The n + 1 error exponent makes a union bound over all 2^n inputs strict.

Equations

• Complexity.NTM.uniformSeedRuns n = 12 * (n + 1) + 1

theorem Complexity.NTM.exists_uniform_correct_seed {k : ℕ} (tm : NTM k) (L : Language) (f : ℕ → ℕ) (haccept : tm.AcceptsWithProb L f (2 / 3)) (hreject : tm.RejectsWithProb L f (1 / 3)) (n : ℕ) : ∃ (seed : BitString (uniformSeedRuns n * f n)), ∀ (x : BitString n), blockMajority (tm.repeatAcceptEvent x.toList (f n)) seed = true ↔ x.toList ∈ L

For every input length, one compact amplified seed gives the correct majority verdict on every input of that length.