Lautemann verifier construction from the two shifted-cover lemmas

Proved

SipserGacsLautemann.amplified_verifier_implies_sigma_two_of_cover_lemmas

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

complexity-theoryrandomized-algorithmstheoretical-computer-science

Let L have a polynomial-randomness, deterministic polynomial-time verifier with two-sided error at most 2^{-(|x|+1)}. Assume the two exact shifted-cover principles used by Lautemann: small sets cannot cover the Boolean cube with too few XOR translates, while sufficiently dense sets admit a covering tuple under the exact union-bound inequality. Then L lies in Sigma-2-P.

This theorem isolates the remaining arithmetic, encoding, finite-exception, and multitape-machine construction after the two combinatorial cover propositions have been supplied explicitly.

Preamble

import Definitions.Def_sipser_gacs_lautemann

Formal statement

namespace SipserGacsLautemann

theorem amplified_verifier_implies_sigma_two_of_cover_lemmas
    (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))))
    (smallCoverObstruction :
      ∀ {n shifts : Nat} (set : BitString n → Prop) [DecidablePred set],
        shifts * setCard set < Fintype.card (BitString n) →
          ∀ translations : Fin shifts → BitString n,
            ¬ shiftedCover set translations)
    (largeCoverExistence :
      ∀ {n shifts : Nat} (set : BitString n → Prop) [DecidablePred set],
        Fintype.card (BitString n) *
              (Fintype.card (BitString n) - setCard set) ^ shifts <
            (Fintype.card (BitString n)) ^ shifts →
          ∃ translations : Fin shifts → BitString n,
            shiftedCover set translations) :
    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