Polynomial-time decidability is preserved by an unused tape
ProvedSipserGacsLautemann.decidesInPolynomialTime_add_unused_tapecomplexity-theorytheoretical-computer-scienceturing-machines
If a predicate on a fixed collection of input tapes is decidable in polynomial time in the mission’s concrete machine model, then the predicate obtained by adding one ignored final tape is also decidable in polynomial time.
The proof constructs the lifted machine explicitly, proves that projecting away the added tape commutes with every step and complete run, establishes stable halting, and replaces the possibly non-monotone original time witness by its displayed polynomial upper bound. This last point is necessary because the ignored tape still contributes to total input length.
Preamble
import Definitions.Def_sipser_gacs_lautemann import Mathlib.Algebra.BigOperators.Fin
Formal statement
namespace SipserGacsLautemann
theorem decidesInPolynomialTime_add_unused_tape {tapes : Nat}
{predicate : (Fin tapes → List Bool) → Prop}
(hpredicate : DecidesInPolynomialTime predicate) :
DecidesInPolynomialTime
(fun input : Fin (tapes + 1) → List Bool =>
predicate (fun i => input i.castSucc)) := by sorry
end SipserGacsLautemannSource
Derived directly from the concrete Machine and DecidesInPolynomialTime definitions in the Sipser–Gács–Lautemann mission.