Polynomial-time closure for the Lautemann shifted-cover verifier

Proved

SipserGacsLautemann.cover_verifier_decides_in_polynomial_time

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

Let $V(x,r)$ be a Boolean predicate decided in polynomial time by the mission's deterministic two-tape Turing-machine model. Given an input $x$ , an encoded list of translations $e$ , and a universal string $u$ , decode $|u|+1$ translations $t_0,\ldots,t_{|u|}$ of width $|u|$ . Then the shifted-cover predicate

C_V(x,e,u)=\bigvee_{i=0}^{|u|} V\bigl(x,u\mathbin{\oplus}t_i\bigr)

is decidable in polynomial time. Bits outside the supplied encoding are read as zero, exactly as prescribed by the mission's decoding function.

This is the computational closure lemma for the Lautemann-cover half of the Sipser–Gács–Lautemann formalization. It requires only $|u|+1$ simulations of the verifier machine, plus polynomial-time decoding and bitwise exclusive-or.

Formalization Note The decoded translations and existential test are exactly decodeCoverTranslationConstruction and coverVerifierConstruction.

Preamble

import Definitions.Def_sipser_gacs_lautemann
import Definitions.Def_sgl_verifier_constructions

Formal statement

namespace SipserGacsLautemann

theorem cover_verifier_decides_in_polynomial_time
    (verifier : List Bool → List Bool → Bool)
    (hverifier :
      DecidesInPolynomialTime
        (fun input : Fin 2 → List Bool =>
          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

Prove2me mission “The Sipser–Gács–Lautemann Theorem”, computational-closure frontier theorem af8010b9-bcbc-4b35-bc70-beb74d64f2bf, https://beta.prove2.me/

View graph