Bounded-error probabilistic computation has polynomial-size circuits

For each input length, finite amplification supplies one seed that is correct simultaneously on every input of that length. Fixing that seed in a parallel bounded-acceptance circuit produces a polynomial-size nonuniform family. The serialized circuit evaluator then turns that family into a polynomial-advice decider.

Main results

• NTM.uniformCorrectSeed_correct: correctness of the selected seed.
• NTM.hardwiredAmplificationFamily_function_iff: fixed-length semantics.
• NTM.hardwiredAmplificationFamily_decides: whole-language correctness.
• NTM.hardwiredAmplificationFamily_size_bigO: quantitative size bound.
• BPP_subset_PPoly: every language in BPP has polynomial-size circuits.
• BPP_subset_PAdvice: every language in BPP has a polynomial-advice decider.

theorem Complexity.NTM.uniformCorrectSeed_correct {k : ℕ} (tm : NTM k) (L : Language) (f : ℕ → ℕ) (haccept : tm.AcceptsWithProb L f (2 / 3)) (hreject : tm.RejectsWithProb L f (1 / 3)) (n : ℕ) (x : BitString n) : blockMajority (tm.repeatAcceptEvent x.toList (f n)) (tm.uniformCorrectSeed L f haccept hreject n) = true ↔ x.toList ∈ L

The selected seed returns the correct amplified verdict on every input of its designated length.

theorem Complexity.NTM.hardwiredAmplificationFamily_function_iff {k : ℕ} (tm : NTM k) (L : Language) (f : ℕ → ℕ) (haccept : tm.AcceptsWithProb L f (2 / 3)) (hreject : tm.RejectsWithProb L f (1 / 3)) (n : ℕ) (x : BitString n) : (tm.hardwiredAmplificationFamily L f haccept hreject).function n x = true ↔ x.toList ∈ L

The hardwired family agrees with L on every fixed-length input.

theorem Complexity.NTM.hardwiredAmplificationFamily_decides {k : ℕ} (tm : NTM k) (L : Language) (f : ℕ → ℕ) (haccept : tm.AcceptsWithProb L f (2 / 3)) (hreject : tm.RejectsWithProb L f (1 / 3)) : (tm.hardwiredAmplificationFamily L f haccept hreject).Decides L

The hardwired amplification family decides the original language.

theorem Complexity.NTM.hardwiredAmplificationFamily_size_bigO {k : ℕ} (tm : NTM k) (L : Language) {f : ℕ → ℕ} {d : ℕ} (haccept : tm.AcceptsWithProb L f (2 / 3)) (hreject : tm.RejectsWithProb L f (1 / 3)) (hf : BigO f fun (x : ℕ) => x ^ d) : BigO (tm.hardwiredAmplificationFamily L f haccept hreject).size fun (x : ℕ) => x ^ (3 * d + 4)

If the original fixed-time horizon is O(n^d), the hardwired amplified family has size O(n^(3d+4)).

theorem Complexity.BPP_subset_PPoly : BPP ⊆ PPoly

BPP ⊆ P/poly: amplify to inverse-exponential error, select one seed that is correct on all inputs of each length, and hardwire that seed into a parallel bounded-acceptance circuit.

theorem Complexity.BPP_subset_PAdvice : BPP ⊆ PAdvice

BPP ⊆ PAdvice: the polynomial-size family supplied by nonuniform derandomization is evaluated using its length-dependent encoding as advice.