Preprocess one cover shift onto the selected verifier tape

Proved

SipserGacsLautemann.cover_single_shift_query_preprocesses_to_selected_verifier_tapes

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

complexity-theorypreprocessingsipser-gacs-lautemannturing-machines

Assume the verifier predicate $V(x,r)$ is decidable in polynomial time when $x$ is on tape $0$ and $r$ is on tape $2$ of a four-tape input. Then the predicate obtained by computing the single decoded cover shift

r = u \oplus t_i

from tapes $(x,e,u,o)$ is also decidable in polynomial time, where $i=\min(|o|,|u|)$ and $t_i$ is decoded from the encoded translation list $e$ using the mission’s cover decoder.

This isolates the remaining preprocessing construction for one Lautemann cover query.

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
    (verifier : List Bool → List Bool → Bool)
    (hselected :
      DecidesInPolynomialTime
        (fun input : Fin 4 → List Bool =>
          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 decomposition lemma for the Prove2me mission “The Sipser–Gács–Lautemann Theorem”, isolating one decoded XOR-shift preprocessing step.

View graph