Single-shift preprocessor delegates up to observational tape equivalence

Proved

SipserGacsLautemann.cover_single_shift_query_preprocessor_obseq_delegates_to_selected_verifier_machine

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

complexity-theorysipser-gacs-lautemannturing-machines

For any four-tape base machine, there is a finite-state preprocessing/delegation machine for the single decoded cover-shift query that reaches a base-machine configuration observationally equivalent to the transformed initial configuration.

The transformed virtual input is

(x,e,u,o) \mapsto (x,e,u\oplus t_i,o),

where $t_i$ is the block decoded from $e$ using $i=\min(|o|,|u|)$ . The theorem intentionally asks only for observational equivalence of tapes, not literal equality of Lean’s zipper representation. This permits harmless extra blank cells left by scans while still guaranteeing that all subsequent base-machine executions have the same accepting/rejecting behavior.

Preamble

import Definitions.Def_sgl_cover_preprocess_transform
import Definitions.Def_sgl_preprocess_delegate_obseq_full

Formal statement


namespace SipserGacsLautemann

theorem cover_single_shift_query_preprocessor_obseq_delegates_to_selected_verifier_machine
    (states : Nat)
    (machine : Machine 4 states) :
    ∃ (State : Type) (_ : Fintype State)
      (preMachine : TypedMachine 4 State)
      (preTime : Nat → Nat)
      (embed : Configuration 4 states →
        TypedConfiguration 4 State)
      (preConfig : (Fin 4 → List Bool) →
        Configuration 4 states),
      PolynomiallyBounded preTime ∧
        (∀ input : Fin 4 → List Bool,
          Configuration.ObsEq (preConfig input)
            (initialConfiguration machine
              (coverSingleShiftPreprocessInput input))) ∧
        (∀ input : Fin 4 → List Bool,
          preMachine.run input
              (preTime (totalInputLength input)) =
            embed (preConfig input)) ∧
        (∀ configuration : Configuration 4 states,
          preMachine.step (embed configuration) =
            embed (machine.step configuration)) ∧
        (∀ configuration : Configuration 4 states,
          preMachine.result (embed configuration).state =
            machine.result configuration.state) := by
  sorry

end SipserGacsLautemann

Source

Prove2me Sipser--Gács--Lautemann mission; replacement for exact-reset single-shift preprocessing using observational tape equivalence.

View graph