Polynomial-time aggregation of verifier calls

Proved

SipserGacsLautemann.polynomial_time_verifier_aggregation

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

bppcomplexity-theorypolynomial-timeturing-machine

Let $V(x,r)$ be a Boolean predicate decided by the mission’s fixed-tape deterministic Turing-machine model in polynomial time. Then both of the following predicates are decidable in polynomial time: (1) the uniform logarithmic-depth ternary-majority evaluation of polynomially many independent calls to $V$ , where the leaf width is inferred from the supplied random string; and (2) the Lautemann shifted-cover predicate, which tests whether at least one of $|u|+1$ decoded translations makes $V(x,u\oplus t_i)$ accept. This is the shared computational closure lemma needed by both remaining SGL frontier nodes.

Preamble

import Definitions.Def_sipser_gacs_lautemann
import Definitions.Def_sgl_verifier_constructions

Formal statement


namespace SipserGacsLautemann

theorem polynomial_time_verifier_aggregation
    (verifier : List Bool → List Bool → Bool)
    (hverifier :
      DecidesInPolynomialTime
        (fun input : Fin 2 → List Bool =>
          verifier (input 0) (input 1) = true)) :
    DecidesInPolynomialTime
        (fun input : Fin 2 → List Bool =>
          ternaryAmplifiedVerifierConstruction verifier
            (input 0) (input 1) = true) ∧
      DecidesInPolynomialTime
        (fun input : Fin 3 → List Bool =>
          coverVerifierConstruction (input 2).length verifier
            (input 0) (input 1) (input 2) = true) := by
  sorry

end SipserGacsLautemann

Source

Standard closure of deterministic polynomial time under polynomially bounded iteration and Boolean aggregation, specialized to the verifier constructions in the Sipser–Gács–Lautemann proof.

View graph