Majority amplification of a bounded-error verifier

Proved

SipserGacsLautemann.bounded_error_verifier_amplification

by Henry Yuen · Jul 24, 2026 · Mathlib c5ea003 (Lean v4.30.0)

complexity-theoryrandomized-algorithmstheoretical-computer-science

Given a polynomial-randomness deterministic polynomial-time verifier with the usual BPP two-sided 2/3 versus 1/3 gap, construct another polynomial-randomness deterministic polynomial-time verifier whose error on every input x is at most 2^{-(|x|+1)}.

This theorem isolates the majority-repetition core: choose polynomially many independent repetitions, encode their random strings on one random tape, decide the majority outcome on the custom two-tape machine, prove the new random-tape and running-time bounds, and establish the exact finite counting tail inequality on both positive and negative inputs.

Preamble

import Definitions.Def_sipser_gacs_lautemann

Formal statement


namespace SipserGacsLautemann

theorem bounded_error_verifier_amplification
    (language : Language)
    (randomBits : Nat → Nat)
    (verifier : List Bool → List Bool → Bool)
    (hrandomBits : PolynomiallyBounded randomBits)
    (hverifier :
      DecidesInPolynomialTime
        (fun input : Fin 2 → List Bool => verifier (input 0) (input 1) = true))
    (hboundedError :
      ∀ input : List Bool,
        (input ∈ language →
          3 * acceptingCard verifier input (randomBits input.length) ≥
            2 * Fintype.card (BitString (randomBits input.length))) ∧
        (input ∉ language →
          3 * rejectingCard verifier input (randomBits input.length) ≥
            2 * Fintype.card (BitString (randomBits input.length)))) :
    ∃ (amplifiedRandomBits : Nat → Nat)
        (amplifiedVerifier : List Bool → List Bool → Bool),
      PolynomiallyBounded amplifiedRandomBits ∧
      DecidesInPolynomialTime
        (fun input : Fin 2 → List Bool =>
          amplifiedVerifier (input 0) (input 1) = true) ∧
      ∀ input : List Bool,
        (input ∈ language →
          2 ^ (input.length + 1) *
              rejectingCard amplifiedVerifier input
                (amplifiedRandomBits input.length) ≤
            Fintype.card
              (BitString (amplifiedRandomBits input.length))) ∧
        (input ∉ language →
          2 ^ (input.length + 1) *
              acceptingCard amplifiedVerifier input
                (amplifiedRandomBits input.length) ≤
            Fintype.card
              (BitString (amplifiedRandomBits input.length))) := by sorry

end SipserGacsLautemann

Source

James Aspnes, Notes on Computational Complexity Theory (2017), Section 12.2, pages 90–91, and Theorem 12.3.1, 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), pages 215–217, https://doi.org/10.1016/0020-0190(83)90044-3

View graph