Blank work tapes may be assumed freely
ProvedSipserGacsLautemann.scratch_tape_provisioningA predicate decidable in polynomial time by a machine granted any fixed number of blank work tapes is decidable in polynomial time in the mission's own sense, with no extra tapes at all.
This is the licence to program the machine model normally. As stated, DecidesInPolynomialTime hands a construction exactly as many tapes as the predicate has arguments, every one of them already holding a piece of the input; there is nowhere to put a counter, an intermediate string, or the answer of a subroutine. With this theorem one may write a machine that helps itself to as much blank working storage as convenient and still conclude membership in the class.
The statement is the natural notion of a conservative extension: at zero scratch tapes the hypothesis is literally the conclusion, and each additional tape is removed by the classical multitape simulation at polynomial cost.
import Definitions.Def_sgl_scratch_tapes
namespace SipserGacsLautemann
theorem scratch_tape_provisioning {tapes : Nat} (scratch : Nat)
(predicate : (Fin tapes → List Bool) → Prop)
(hdecides : DecidesInPolynomialTimeWithScratch scratch predicate) :
DecidesInPolynomialTime predicate := by sorry
end SipserGacsLautemann