Machine-level polynomial-time verifier aggregation scheduler

Proved

SipserGacsLautemann.polynomial_time_verifier_aggregation_from_machine

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

bppcomplexity-theorypolynomial-timeturing-machine

Let $V(x,r)$ be a Boolean predicate whose verifier is given concretely by a two-tape deterministic Turing machine $M$ with a polynomial time bound $T$ , in the exact DecidesInPolynomialTime sense of the mission model. This theorem asserts the machine-level scheduler closure needed for the Sipser--Gács--Lautemann proof: from $M$ one can build polynomial-time deciders for both aggregation predicates:

(x,\rho)\mapsto \operatorname{Maj}_3^{(d)}(V(x,r_1),\ldots,V(x,r_{3^d}))

where $d=\lceil \log_2(|x|+1)\rceil+3$ and the leaves are decoded from the supplied random string, and

(x,e,u)\mapsto \exists i\le |u|\; V(x,u\oplus t_i(e)).

This is the remaining low-level scheduler/loader theorem: it is responsible for preserving the raw input, constructing each derived verifier query, simulating $M$ , and aggregating the answers with polynomial overhead.

Formalization Note This child theorem is deliberately stated after unpacking DecidesInPolynomialTime into the concrete state count, machine, time bound, and correctness proof. The two current frontier theorems are immediate projections of this shared scheduler.

Preamble

import Definitions.Def_sipser_gacs_lautemann
import Definitions.Def_sgl_verifier_constructions

Formal statement

namespace SipserGacsLautemann

theorem polynomial_time_verifier_aggregation_from_machine
    (verifier : List Bool → List Bool → Bool)
    (states : Nat)
    (machine : Machine 2 states)
    (time : Nat → Nat)
    (htime : PolynomiallyBounded time)
    (hcorrect :
      ∀ input : Fin 2 → List Bool,
        (machine.acceptsWithin input
            (time (totalInputLength input)) ↔
          verifier (input 0) (input 1) = true) ∧
        (machine.rejectsWithin input
            (time (totalInputLength input)) ↔
          ¬ 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 deterministic polynomial-time closure under polynomially bounded iteration and Boolean aggregation, specialized to the Sipser--Gács--Lautemann verifier constructions and the mission custom Turing-machine model.

View graph