Amplified BPP verifiers yield a Sigma-2-P characterization

Proved

SipserGacsLautemann.amplified_verifier_implies_sigma_two

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

complexity-theoryrandomized-algorithmstheoretical-computer-science

Let L have a deterministic polynomial-time randomized verifier using a polynomially bounded number of random bits. Assume that, on every input x, the verifier's error fraction is at most 2^{-(|x|+1)} on both members and nonmembers of L. Then L lies in Sigma-2-P.

This theorem isolates the second half of Lautemann's argument after amplification: encode polynomially many XOR translations existentially, quantify universally over a point of the random-bit cube, and use the shifted-cover density gap to distinguish members from nonmembers. The construction also packages the resulting three-tape verifier and its polynomial time bound.

Preamble

import Definitions.Def_sipser_gacs_lautemann

Formal statement

namespace SipserGacsLautemann

theorem amplified_verifier_implies_sigma_two
    (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))
    (herror :
      ∀ 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)))) :
    InSigmaTwoP language := by sorry

end SipserGacsLautemann

Source

James Aspnes, Notes on Computational Complexity Theory (2017), Section 12.3, Theorem 12.3.1, page 92, https://www.cs.yale.edu/homes/aspnes/classes/468/notes-2017.pdf; Jonathan Katz, Notes on Complexity Theory, Lecture 7 (2005), Section 2.2.1, Propositions 6–7, pages 7-2–7-3, https://www.cs.umd.edu/~jkatz/complexity/f05/lecture7.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