Machine-level shifted-cover verifier scheduler

Proved

SipserGacsLautemann.cover_verifier_decides_from_machine

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

bppcomplexity-theorypolynomial-timeturing-machine

Let $V(x,r)$ be decided by a concrete two-tape deterministic Turing machine $M$ with polynomial time bound $T$ , in the exact sense used by DecidesInPolynomialTime. This theorem asserts the machine-level construction for the shifted-cover verifier: given input $x$ , encoded translations $e$ , and universal point $u$ , the predicate that tests whether some decoded shift makes $V(x,u \oplus t_i(e))$ accept is decidable in polynomial time.

This isolates the shifted-cover scheduler/loader/controller part of the remaining Sipser--Gács--Lautemann aggregation proof.

Preamble

import Definitions.Def_sipser_gacs_lautemann
import Definitions.Def_sgl_verifier_constructions

Formal statement

namespace SipserGacsLautemann

theorem cover_verifier_decides_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 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 many scheduled verifier calls, specialized to the Lautemann shifted-cover verifier in the Sipser--Gács--Lautemann proof.

View graph