Complexity classes for the Sipser–Gács–Lautemann theorem

Definition

sipser_gacs_lautemann

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

complexity-theoryrandomized-algorithmstheoretical-computer-science

This module gives a concrete computational model for the theorem. A language is a set of finite Boolean strings. Deterministic polynomial time is defined using finite-state multitape Turing machines whose tapes have a binary alphabet and a blank symbol. A machine must halt with the correct Boolean answer within a polynomial bound in the total input length. BPP uses a polynomial-length random tape and the usual two-sided acceptance gap of $2/3$ versus $1/3$ . The classes $\Sigma_2^P$ and $\Pi_2^P$ use polynomial-length existential and universal witnesses in the respective quantifier orders. The module also defines bitwise XOR, translated subsets of the Boolean cube, shifted covers, and exact acceptance counts.\n\nThese definitions provide a reusable, uniform foundation for formalizing probabilistic and alternating complexity arguments without treating polynomial-time computability as an opaque predicate.\n\nFormalization Note Inputs to a verifier occupy separate tapes, avoiding any dependence on a choice of pairing or delimiter encoding. Halting configurations are stable under further machine steps.

Definition code

import Mathlib.Data.Fin.Basic
import Mathlib.Data.Finset.Card
import Mathlib.Data.Fintype.Card
import Mathlib.Data.Fintype.Pi
import Mathlib.Data.List.Basic

namespace SipserGacsLautemann

inductive TapeSymbol where
  | blank
  | bit (value : Bool)
  deriving DecidableEq

inductive HeadMove where
  | left
  | stay
  | right
  deriving DecidableEq

structure Tape where
  left : List TapeSymbol
  head : TapeSymbol
  right : List TapeSymbol

namespace Tape

def ofBits : List Bool → Tape
  | [] => ⟨[], .blank, []⟩
  | b :: bs => ⟨[], .bit b, bs.map .bit⟩

def write (tape : Tape) (symbol : TapeSymbol) : Tape :=
  { tape with head := symbol }

def move : Tape → HeadMove → Tape
  | tape, .stay => tape
  | ⟨[], head, right⟩, .left => ⟨[], .blank, head :: right⟩
  | ⟨symbol :: left, head, right⟩, .left =>
      ⟨left, symbol, head :: right⟩
  | ⟨left, head, []⟩, .right => ⟨head :: left, .blank, []⟩
  | ⟨left, head, symbol :: right⟩, .right =>
      ⟨head :: left, symbol, right⟩

end Tape

/-- A deterministic multitape Turing machine with a finite state space. -/
structure Machine (tapes states : Nat) where
  start : Fin states
  transition :
    Fin states → (Fin tapes → TapeSymbol) →
      Fin states × (Fin tapes → TapeSymbol × HeadMove)
  result : Fin states → Option Bool

structure Configuration (tapes states : Nat) where
  state : Fin states
  tape : Fin tapes → Tape

def initialConfiguration {tapes states : Nat} (machine : Machine tapes states)
    (input : Fin tapes → List Bool) : Configuration tapes states :=
  ⟨machine.start, fun i => Tape.ofBits (input i)⟩

def Machine.step {tapes states : Nat} (machine : Machine tapes states)
    (configuration : Configuration tapes states) : Configuration tapes states :=
  match machine.result configuration.state with
  | some _ => configuration
  | none =>
      let action := machine.transition configuration.state (fun i => (configuration.tape i).head)
      { state := action.1
        tape := fun i =>
          Tape.move (Tape.write (configuration.tape i) (action.2 i).1) (action.2 i).2 }

def Machine.run {tapes states : Nat} (machine : Machine tapes states)
    (input : Fin tapes → List Bool) : Nat → Configuration tapes states
  | 0 => initialConfiguration machine input
  | steps + 1 => machine.step (machine.run input steps)

def Machine.acceptsWithin {tapes states : Nat} (machine : Machine tapes states)
    (input : Fin tapes → List Bool) (steps : Nat) : Prop :=
  machine.result (machine.run input steps).state = some true

def Machine.rejectsWithin {tapes states : Nat} (machine : Machine tapes states)
    (input : Fin tapes → List Bool) (steps : Nat) : Prop :=
  machine.result (machine.run input steps).state = some false

def totalInputLength {tapes : Nat} (input : Fin tapes → List Bool) : Nat :=
  (List.ofFn fun i => (input i).length).sum

def PolynomiallyBounded (bound : Nat → Nat) : Prop :=
  ∃ coefficient degree : Nat, ∀ n : Nat,
    bound n ≤ coefficient * (n + 1) ^ degree

def DecidesInPolynomialTime {tapes : Nat}
    (predicate : (Fin tapes → List Bool) → Prop) : Prop :=
  ∃ (states : Nat) (machine : Machine tapes states) (time : Nat → Nat),
    PolynomiallyBounded time ∧
      ∀ input : Fin tapes → List Bool,
        (machine.acceptsWithin input (time (totalInputLength input)) ↔ predicate input) ∧
        (machine.rejectsWithin input (time (totalInputLength input)) ↔ ¬predicate input)

abbrev Language := Set (List Bool)
abbrev BitString (n : Nat) := Fin n → Bool

def BitString.toList {n : Nat} (bits : BitString n) : List Bool :=
  List.ofFn bits

def xor {n : Nat} (x y : BitString n) : BitString n :=
  fun i => x i != y i

def shiftedCover {n shifts : Nat} (set : BitString n → Prop)
    (translations : Fin shifts → BitString n) : Prop :=
  ∀ point : BitString n, ∃ i : Fin shifts, set (xor point (translations i))

def setCard {n : Nat} (set : BitString n → Prop) [DecidablePred set] : Nat :=
  (Finset.univ.filter set).card

def acceptingCard (verifier : List Bool → List Bool → Bool)
    (input : List Bool) (randomBits : Nat) : Nat :=
  (Finset.univ.filter fun random : BitString randomBits =>
    verifier input random.toList = true).card

def rejectingCard (verifier : List Bool → List Bool → Bool)
    (input : List Bool) (randomBits : Nat) : Nat :=
  (Finset.univ.filter fun random : BitString randomBits =>
    verifier input random.toList = false).card

def InBPP (language : Language) : Prop :=
  ∃ (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 →
        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)))

def InSigmaTwoP (language : Language) : Prop :=
  ∃ (existentialBits universalBits : Nat → Nat)
      (verifier : List Bool → List Bool → List Bool → Bool),
    PolynomiallyBounded existentialBits ∧
    PolynomiallyBounded universalBits ∧
    DecidesInPolynomialTime
      (fun input : Fin 3 → List Bool => verifier (input 0) (input 1) (input 2) = true) ∧
    ∀ input : List Bool,
      input ∈ language ↔
        ∃ existential : BitString (existentialBits input.length),
          ∀ universal : BitString (universalBits input.length),
            verifier input existential.toList universal.toList = true

def InPiTwoP (language : Language) : Prop :=
  ∃ (universalBits existentialBits : Nat → Nat)
      (verifier : List Bool → List Bool → List Bool → Bool),
    PolynomiallyBounded universalBits ∧
    PolynomiallyBounded existentialBits ∧
    DecidesInPolynomialTime
      (fun input : Fin 3 → List Bool => verifier (input 0) (input 1) (input 2) = true) ∧
    ∀ input : List Bool,
      input ∈ language ↔
        ∀ universal : BitString (universalBits input.length),
          ∃ existential : BitString (existentialBits input.length),
            verifier input universal.toList existential.toList = true

end SipserGacsLautemann

Source

James Aspnes, Notes on Computational Complexity Theory (2017), Chapters 2 and 12, especially §§12.2–12.3, 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