Nonuniform derandomization — definitions

This module defines the explicit nonuniform circuit-family witness used in BPP ⊆ P/poly. For each input length it chooses a uniformly correct amplified seed and fixes that seed in the canonical choices-first acceptance circuit.

Correctness, size bounds, and the containment theorem are proved in the internal and surface modules.

noncomputable def Complexity.NTM.uniformCorrectSeed {k : ℕ} (tm : NTM k) (L : Language) (f : ℕ → ℕ) (haccept : tm.AcceptsWithProb L f (2 / 3)) (hreject : tm.RejectsWithProb L f (1 / 3)) (n : ℕ) : BitString (uniformSeedRuns n * f n)

Choose one amplified seed that is correct simultaneously on every input of length n. Its specification is uniformCorrectSeed_correct.

Equations

• tm.uniformCorrectSeed L f haccept hreject n = Classical.choose ⋯

noncomputable def Complexity.NTM.hardwiredAmplificationFamily {k : ℕ} (tm : NTM k) (L : Language) (f : ℕ → ℕ) (haccept : tm.AcceptsWithProb L f (2 / 3)) (hreject : tm.RejectsWithProb L f (1 / 3)) : CircuitFamily Basis.andOr2

The circuit family obtained by choosing and fixing one uniformly correct amplified seed at each positive input length. The answer on the unique empty input is stored directly, following the CircuitFamily convention.

Equations

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