Nonuniform derandomization — proof internals

This module proves correctness and polynomial size for the circuit family that hardwires a uniformly correct amplified seed at each input length. Public statements are exposed by Complexitylib.Classes.Randomized.PPoly.

theorem Complexity.NTM.uniformCorrectSeed_correct_internal {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

Internal specification of the chosen uniformly correct seed.

theorem Complexity.NTM.hardwiredAmplificationFamily_function_iff_internal {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

Internal fixed-length correctness theorem for the hardwired family.

theorem Complexity.NTM.hardwiredAmplificationFamily_decides_internal {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

Internal correctness theorem for the hardwired family.

theorem Complexity.NTM.hardwiredAmplificationFamily_size_bigO_internal {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)

Internal polynomial-size accounting for the hardwired amplification family.

theorem Complexity.BPP_subset_PPoly_internal : BPP ⊆ PPoly

Internal proof of BPP ⊆ P/poly.