The final work tape can be simulated away
ProvedSipserGacsLautemann.eliminate_last_scratch_tapeA predicate decidable in polynomial time with a single blank work tape is decidable in polynomial time with none at all — that is, in the mission's own sense.
This is the hard half of tape elimination, and it is where the whole difficulty of the model concentrates. Every surviving tape now carries a component of the input, so the blank tape being removed must be hosted alongside content that is already in place. Hosting it as a second track requires the host tape's own contents to be spread out first, and that re-encoding phase has an awkward flavour: positional arithmetic normally wants counters, and counters normally want the very work tape being provisioned.
The way out is marker-driven rather than counter-driven. The alphabet has only the three symbols blank, and , so a head position cannot be marked by a fresh symbol; but once each simulated cell is widened into a block of physical cells, spare codes become available and can serve as both head flags and the marker separating processed from unprocessed tape. Spreading then proceeds by repeatedly locating the leftmost unprocessed symbol and shifting the suffix, times at each.
Only polynomial overhead is needed, so no efficiency is at stake — the crude bound is the right one, being the easiest to prove.
import Definitions.Def_sgl_scratch_tapes
namespace SipserGacsLautemann
theorem eliminate_last_scratch_tape {tapes : Nat}
(predicate : (Fin tapes → List Bool) → Prop)
(hdecides : DecidesInPolynomialTimeWithScratch 1 predicate) :
DecidesInPolynomialTimeWithScratch 0 predicate := by sorry