Machine-level preprocessing for one decoded cover shift

Proved

SipserGacsLautemann.cover_single_shift_query_preprocesses_to_selected_verifier_tapes_from_machine

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

complexity-theorypreprocessingsipser-gacs-lautemannturing-machines

Let a concrete four-tape machine decide the selected-tape verifier predicate $V(x,r)$ , where $x$ is on tape $0$ and $r$ is on tape $2$ . This theorem asserts that a polynomial-time machine can preprocess a four-tape input $(x,e,u,o)$ by decoding the cover translation indexed by $\min(|o|,|u|)$ from $e$ , forming the XOR query $u\oplus t_i$ , and then invoking the selected-tape verifier machine.

This is the machine-level preprocessing construction for one shifted-cover verifier call.

Preamble

import Definitions.Def_sipser_gacs_lautemann
import Definitions.Def_sgl_verifier_constructions

Formal statement

namespace SipserGacsLautemann

theorem cover_single_shift_query_preprocesses_to_selected_verifier_tapes_from_machine
    (verifier : List Bool → List Bool → Bool)
    (states : Nat)
    (machine : Machine 4 states)
    (time : Nat → Nat)
    (htime : PolynomiallyBounded time)
    (hcorrect :
      ∀ input : Fin 4 → List Bool,
        (machine.acceptsWithin input
            (time (totalInputLength input)) ↔
          verifier (input 0) (input 2) = true) ∧
        (machine.rejectsWithin input
            (time (totalInputLength input)) ↔
          ¬ verifier (input 0) (input 2) = 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 machine-level preprocessing decomposition lemma for the Prove2me mission “The Sipser–Gács–Lautemann Theorem”.

View graph