Single-shift cover query is decidable from the verifier machine

Proved

SipserGacsLautemann.cover_single_shift_query_decides_from_machine

by Henry Yuen · Jul 24, 2026 · Mathlib 0df444a (Lean v4.33.1)

complexity-theoryschedulersipser-gacs-lautemannturing-machines

Let $V(x,r)$ be decided by a deterministic two-tape verifier machine in polynomial time. Given four tapes $(x,e,u,o)$ , interpret the length of the fourth tape as a unary shift offset, capped at $|u|$ . Decode that one translation from the encoded translation list $e$ , XOR it with $u$ , and run $V$ on the resulting query.

This theorem asserts that this single decoded-shift query predicate is decidable in polynomial time. It isolates the query-construction and one-call simulation part of the shifted-cover verifier scheduler.

Preamble

import Definitions.Def_sipser_gacs_lautemann
import Definitions.Def_sgl_verifier_constructions

Formal statement

namespace SipserGacsLautemann

theorem cover_single_shift_query_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 4 → List Bool =>
        verifier (input 0)
          (List.zipWith (· != ·) (input 2)
            (decodeCoverTranslationConstruction
              (input 2).length (input 1)
              ⟨min (input 3).length (input 2).length,
                by
                  exact Nat.lt_succ_of_le
                    (Nat.min_le_right (input 3).length
                      (input 2).length)⟩)) = true) := by
  sorry

end SipserGacsLautemann

Source

Internal decomposition lemma for the Prove2me mission “The Sipser–Gács–Lautemann Theorem”, isolating single decoded-shift query construction for the Lautemann cover verifier.

View graph