Polynomial-time decidability on selected tapes 0 and 2 of four tapes

Proved

SipserGacsLautemann.decidesInPolynomialTime_select_tapes_0_2_of_4

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

complexity-theorytape-reindexingturing-machines

If a predicate on two input tapes is decidable in polynomial time, then the predicate obtained by applying it to tapes $0$ and $2$ of a four-tape input is also decidable in polynomial time.

This is a tape-selection closure lemma. The proof adds two unused tapes to the original two-tape decider and then permutes the four tapes so that the second active input is read from tape $2$ .

Preamble

import Definitions.Def_sipser_gacs_lautemann

Formal statement

namespace SipserGacsLautemann

theorem decidesInPolynomialTime_select_tapes_0_2_of_4
    {predicate : (Fin 2 → List Bool) → Prop}
    (hpredicate : DecidesInPolynomialTime predicate) :
    DecidesInPolynomialTime
      (fun input : Fin 4 → List Bool =>
        predicate (fun i : Fin 2 =>
          if i = 0 then input 0 else input 2)) := by
  sorry

end SipserGacsLautemann

Source

Internal reusable tape-selection closure lemma for the Prove2me mission “The Sipser–Gács–Lautemann Theorem”.

View graph