Space accounting for a machine reading its input off a work tape

TM.retargetInput runs a machine M with its input tape relocated to work tape k. That relocation is exactly what a space bound has to be re-read through: what was M's free input tape becomes a charged work tape, so the window the retargeted machine needs is M's own space budget plus the length of the virtual input.

The correspondence is step-by-step (TM.retargetInput_step_commute), so every configuration the retargeted machine reaches is a wrapped configuration of M — with the real input tape, which it never consults, drifting only by an idle move. M's bound on its own run therefore transfers.

Main results

• TM.retargetInput_within — a wrapped configuration is inside the window when M's is
• TM.retargetInput_keepsWindow_of_reaches — the whole retargeted run stays inside it
• TM.retargetInputStarted_reaches_iff, TM.retargetInputStarted_keepsWindow_of_reaches — the started wrapper runs the same steps, so the accounting carries over
• TM.retargetOutput_keepsWindow_of_reaches — redirecting the output onto a work tape costs one cell of window
• TM.applyTM_keepsWindow_of_reaches — the two composed: the window of the work-to-work evaluator
• TM.applyTM_keepsWindow_of_decidesInSpace — the same from a TM.DecidesInSpace hypothesis
• TM.liftTM_keepsWindow_of_reaches — adding spare work tapes costs no window

theorem Complexity.TM.retargetInput_within {k : ℕ} (M : TM k) (r : Tape) (c : Cfg k M.Q) {m s inputLength space : ℕ} (hc : c.WithinDecisionSpace m s) (hspace : m + s + 1 ≤ space) (hr : r.head ≤ inputLength + space + 1) : (M.retargetWrap r c).WithinDecisionSpace inputLength space

A wrapped configuration sits inside a window as soon as the wrapped M-configuration does: M's work heads and its relocated input head are all charged against the new budget.

theorem Complexity.TM.retargetInput_keepsWindow_of_reaches {k : ℕ} (M : TM k) (r₀ : Tape) (c₀ : Cfg k M.Q) {m s inputLength space : ℕ} (hM : ∀ (c : Cfg k M.Q), M.reaches c₀ c → c.WithinDecisionSpace m s) (hc₀inp : c₀.input.StartInvariant) (hc₀work : ∀ (i : Fin k), (c₀.work i).StartInvariant) (hc₀out : c₀.output.StartInvariant) (hr₀ : r₀.StartInvariant) (hspace : m + s + 1 ≤ space) (hr : max r₀.head 1 ≤ inputLength + space + 1) (d : Cfg (k + 1) M.retargetInput.Q) : M.retargetInput.reaches (M.retargetWrap r₀ c₀) d → d.WithinDecisionSpace inputLength space

The retargeted run stays inside the window. Every configuration reachable from a wrapped start is itself wrapped — the step correspondence is exact — so M's bound on its own run is the only thing needed.

The started wrapper

theorem Complexity.TM.retargetInputStarted_reaches_iff {k : ℕ} (M : TM k) (c d : Cfg (k + 1) M.Q) : M.retargetInputStarted.reaches c d ↔ M.retargetInput.reaches c d

The started wrapper and the plain retargeted machine have the same step relation, so they reach exactly the same configurations. Only their start states differ.

theorem Complexity.TM.retargetInputStarted_keepsWindow_of_reaches {k : ℕ} (M : TM k) (r₀ : Tape) (c₀ : Cfg k M.Q) {m s inputLength space : ℕ} (hM : ∀ (c : Cfg k M.Q), M.reaches c₀ c → c.WithinDecisionSpace m s) (hc₀inp : c₀.input.StartInvariant) (hc₀work : ∀ (i : Fin k), (c₀.work i).StartInvariant) (hc₀out : c₀.output.StartInvariant) (hr₀ : r₀.StartInvariant) (hspace : m + s + 1 ≤ space) (hr : max r₀.head 1 ≤ inputLength + space + 1) (d : Cfg (k + 1) M.retargetInputStarted.Q) : M.retargetInputStarted.reaches (M.retargetWrap r₀ c₀) d → d.WithinDecisionSpace inputLength space

The started wrapper keeps the window too. It runs the same steps as TM.retargetInput, so the accounting of TM.retargetInput_keepsWindow_of_reaches applies verbatim.

Redirecting the output to a work tape

theorem Complexity.TM.retargetOutput_keepsWindow_of_reaches {m : ℕ} (tm : TM m) (c₀ : Cfg m tm.Q) {inputLength space : ℕ} (htm : ∀ (c : Cfg m tm.Q), tm.reaches c₀ c → c.WithinDecisionSpace inputLength space) (D : Cfg (m + 1) tm.retargetOutput.Q) : tm.retargetOutput.reaches (tm.retargetCfg c₀) D → D.WithinDecisionSpace inputLength (space + 1)

Redirecting the output onto a work tape costs one cell. The old output tape becomes work tape n, and the decision convention allows the output head one cell more than the work heads, so the window grows by exactly that. The real output tape is left parked as a dummy.

The work-to-work evaluator

theorem Complexity.TM.applyTM_keepsWindow_of_reaches {k : ℕ} (M : TM k) (r₀ : Tape) (c₀ : Cfg k M.Q) {m s inputLength space : ℕ} (hM : ∀ (c : Cfg k M.Q), M.reaches c₀ c → c.WithinDecisionSpace m s) (hc₀inp : c₀.input.StartInvariant) (hc₀work : ∀ (i : Fin k), (c₀.work i).StartInvariant) (hc₀out : c₀.output.StartInvariant) (hr₀ : r₀.StartInvariant) (hspace : m + s + 1 ≤ space) (hr : max r₀.head 1 ≤ inputLength + space + 1) (D : Cfg (k + 2) M.applyTM.Q) : M.applyTM.reaches (M.retargetInputStarted.retargetCfg (M.retargetWrap r₀ c₀)) D → D.WithinDecisionSpace inputLength (space + 1)

The work-to-work evaluator keeps a window. TM.applyTM M is M retargeted twice — its input read off a work tape, its output written to another — so its window is M's own decision-space budget, plus the virtual input's length for the relocated input tape, plus one cell for the relocated output tape. Every quantity is explicit, so a caller that knows M's polynomial space bound knows this one.

theorem Complexity.TM.applyTM_keepsWindow_of_decidesInSpace {k : ℕ} (M : TM k) {L : Language} {S : ℕ → ℕ} (hdec : M.DecidesInSpace L S) (hne : M.qstart ≠ M.qhalt) (y : List Bool) (realInput : Tape) (hrsi : realInput.StartInvariant) {inputLength space : ℕ} (hspace : y.length + S y.length + 1 ≤ space) (hr : max realInput.head 1 ≤ inputLength + space + 1) (D : Cfg (k + 2) M.applyTM.Q) : M.applyTM.reaches (M.retargetInputStarted.retargetCfg (M.retargetInputStartedCfg y realInput)) D → D.WithinDecisionSpace inputLength (space + 1)

The evaluator's window, from the source machine's space bound alone. Started on the canonical entry configuration with virtual input y, TM.applyTM M stays inside a window of |y| + S |y| + 2 — the source's own budget, the relocated input tape, and one cell for the relocated output. This is the form a caller with a TM.DecidesInSpace hypothesis can use.

Embedding a machine in a larger tape space

theorem Complexity.TM.liftTM_keepsWindow_of_reaches {m' : ℕ} (tm : TM m') (m : ℕ) (c₀ : Cfg m' tm.Q) {inputLength space : ℕ} (hs : 1 ≤ space) (htm : ∀ (c : Cfg m' tm.Q), tm.reaches c₀ c → c.WithinDecisionSpace inputLength space) (D : Cfg (m' + m) (tm.liftTM m).Q) : (tm.liftTM m).reaches (tm.liftCfg m c₀) D → D.WithinDecisionSpace inputLength space

Adding spare work tapes costs no window. TM.liftTM runs a machine unchanged alongside m extra tapes, which stay parked at cell one throughout, so a configuration of the lifted machine sits in exactly the window its underlying configuration does. This is how a subroutine is placed inside a machine with more tapes than it needs.