One blank work tape can be simulated away
ProvedSipserGacsLautemann.eliminate_one_scratch_tapeA predicate decidable in polynomial time by a machine granted blank work tapes is decidable in polynomial time by one granted only .
This is the tape-reduction step of the classical multitape simulation, specialized to a model whose tapes are fixed in number and preloaded with the input. The one tape being removed starts empty, so nothing has to be gathered: its contents may be hosted inside the blank region lying to the left of the input on a surviving tape, provided the simulating machine tracks that tape's head position. Because the alphabet has only the three symbols blank, and , a head position cannot be marked by a fresh symbol and must instead be recorded by widening each simulated cell into a fixed-size block of physical cells.
Only a polynomial overhead is required, so the crude simulation suffices: each simulated step costs a sweep of the region used so far, and the region grows by at most one cell per step, giving a quadratic blow-up in the running time.
This is the single obstruction standing between the mission's machine model and ordinary structured programming. Iterating it discharges any number of work tapes, so it is the only theorem needed for full scratch provisioning — and it is needed independently of this mission, since without it the model cannot even express that polynomial time is closed under intersection.
import Definitions.Def_sgl_scratch_tapes
namespace SipserGacsLautemann
theorem eliminate_one_scratch_tape {tapes : Nat} (scratch : Nat)
(predicate : (Fin tapes → List Bool) → Prop)
(hdecides : DecidesInPolynomialTimeWithScratch (scratch + 1) predicate) :
DecidesInPolynomialTimeWithScratch scratch predicate := by sorry
end SipserGacsLautemann