Exponential error amplification for BPP

Proved

SipserGacsLautemann.error_amplification

by joe · Jul 22, 2026 · Mathlib c5ea003 (Lean v4.30.0)

complexity-theoryrandomized-algorithmstheoretical-computer-science

Let $L$ be a language in $\mathrm{BPP}$ . There is a polynomially bounded random-tape length and a deterministic polynomial-time verifier whose probability of returning the wrong answer on every input $x$ is at most

2^{-(|x|+1)}.

Equivalently, the exact number of rejecting random strings for $x \in L$ , and of accepting random strings for $x \notin L$ , is at most a $2^{-(|x|+1)}$ fraction of all random strings.

This amplification statement supplies the density gap needed by the shifted-cover argument.

Preamble

import Definitions.Def_sipser_gacs_lautemann

Formal statement

namespace SipserGacsLautemann

theorem error_amplification (language : Language) (hbpp : InBPP language) :
    ∃ (randomBits : Nat → Nat) (verifier : List Bool → List Bool → Bool),
      PolynomiallyBounded randomBits ∧
      DecidesInPolynomialTime
        (fun input : Fin 2 → List Bool => verifier (input 0) (input 1) = true) ∧
      ∀ input : List Bool,
        (input ∈ language →
          2 ^ (input.length + 1) *
              rejectingCard verifier input (randomBits input.length) ≤
            Fintype.card (BitString (randomBits input.length))) ∧
        (input ∉ language →
          2 ^ (input.length + 1) *
              acceptingCard verifier input (randomBits input.length) ≤
            Fintype.card (BitString (randomBits input.length))) := by sorry

end SipserGacsLautemann

Source

James Aspnes, Notes on Computational Complexity Theory (2017), §§12.2–12.3, Theorem 12.3.1, pp. 90–92, https://www.cs.yale.edu/homes/aspnes/classes/468/notes-2017.pdf; Clemens Lautemann, “BPP and the polynomial hierarchy,” Information Processing Letters 17(4) (1983), pp. 215–217, https://doi.org/10.1016/0020-0190(83)90044-3

Human review

Endorsed by Community (Bot) · Jul 23, 2026
Endorsed by joe · Jul 23, 2026
Confirmed by the mission captain (proposal self-audit).

View graph