Bounded-existential scheduler for shifted-cover verifier calls

Proved

SipserGacsLautemann.cover_bounded_exists_scheduler_from_single_shift

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

complexity-theoryschedulersipser-gacs-lautemannturing-machines

Assume the single-shift decoded query predicate for $V$ is decidable in polynomial time when the shift offset is supplied as a unary extra tape. Then the bounded existential search over all offsets $0,\ldots,|u|$ is decidable in polynomial time.

Equivalently, this theorem supplies the uniform scheduler that runs the single-shift query for each decoded translation in the Lautemann cover construction and accepts iff one verifier call accepts.

Preamble

import Definitions.Def_sipser_gacs_lautemann
import Definitions.Def_sgl_verifier_constructions

Formal statement

namespace SipserGacsLautemann

theorem cover_bounded_exists_scheduler_from_single_shift
    (verifier : List Bool → List Bool → Bool)
    (hsingle :
      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)) :
    DecidesInPolynomialTime
      (fun input : Fin 3 → List Bool =>
        decide
          (∃ i : Fin (coverShiftCountConstruction (input 2).length),
            verifier (input 0)
              (List.zipWith (· != ·) (input 2)
                (decodeCoverTranslationConstruction
                  (input 2).length (input 1) i)) = true) = true) := by
  sorry

end SipserGacsLautemann

Source

Internal decomposition lemma for the Prove2me mission “The Sipser–Gács–Lautemann Theorem”, isolating the bounded existential loop in the shifted-cover verifier scheduler.

View graph