Multi-tape → single-tape simulation

A nondeterministic machine with k work tapes can be simulated by one with a single work tape, preserving the decided language with only polynomial time overhead (the classic O(T²) multi-tape-to-single-tape simulation).

This is a reusable robustness lemma:

• Cook–Levin (SAT/CookLevin.lean) uses it so the computation-tableau formula only has to track one work tape instead of k.
• Universal machines are far simpler to construct when they need only simulate a single-work-tape machine.

Decomposition

• singleTapeSim N : NTM 1 — the simulating machine (SingleTape/Sim.lean), for k ≥ 1; 0-work-tape machines are handled by padding (Pad.lean).
• singleTapeSimTime k T — the explicit time bound 16·(k+1)·(T n + n + 1)².
• singleTapeSim_allPathsHaltIn, singleTapeSim_acceptsInTime_iff — the two behavioural facts (timing + acceptance equivalence), assembled from the forward (acceptsInTime_singleTapeSim_of_acceptsInTime) and reverse (halted_singleTapeSim_of_trace_qhalt) correspondence theorems of SingleTape/Correctness.lean.
• singleTapeSimTime_bigO — the overhead stays polynomial.

singleTapeSim_decidesInTime and exists_singleTape_decidesInTime are assembled from these.

def Complexity.NTM.singleTapeSimTime (k : ℕ) (T : ℕ → ℕ) : ℕ → ℕ

Time overhead of the single-tape simulation: the classic quadratic blow-up (T + n + 1)², times a per-machine constant 16·(k+1) that absorbs the block width (each super-position is 3k cells) and the four sweeps per simulated step. The constant is deliberately generous. Downstream results use both the =O class (singleTapeSimTime_bigO) and the explicit formula: the universal machine's clock (TM.utmTM_simulates_pair) states the same quadratic 16(k+1)(t+|p|+1)², and the time hierarchy theorem (time_hierarchy_weak) unfolds it.

Equations

• Complexity.NTM.singleTapeSimTime k T n = 16 * (k + 1) * (T n + n + 1) ^ 2

theorem Complexity.NTM.singleTapeSimTime_bigO {k : ℕ} {T : ℕ → ℕ} {c : ℕ} (hTO : BigO T fun (x : ℕ) => x ^ c) : BigO (singleTapeSimTime k T) fun (x : ℕ) => x ^ (2 * c + 2)

The simulation's time overhead stays polynomial.

theorem Complexity.NTM.singleTapeSim_allPathsHaltIn {k : ℕ} (N : NTM k) (hk : 1 ≤ k) {T : ℕ → ℕ} (hN : N.AllPathsHaltIn T) : N.singleTapeSim.AllPathsHaltIn (singleTapeSimTime k T)

The simulator halts on all computation paths within the overhead time bound, whenever N does: an arbitrary simulator choice stream induces an N-run (read off at the closed-form decision positions), N halts on it within T, and the simulator then halts right after its corresponding macro-step (SingleTape.halted_singleTapeSim_of_trace_qhalt).

theorem Complexity.NTM.singleTapeSim_acceptsInTime_iff {k : ℕ} (N : NTM k) (hk : 1 ≤ k) (T : ℕ → ℕ) (hN : N.AllPathsHaltIn T) (x : List Bool) : N.singleTapeSim.AcceptsInTime x (singleTapeSimTime k T x.length) ↔ N.AcceptsInTime x (T x.length)

The simulator accepts x within the overhead time bound iff N accepts x within its original time bound.

The all-paths-halt hypothesis hN is necessary for the forward direction: the simulator's quadratic budget 16(k+1)(T+n+1)² leaves room to complete N-runs longer than T n, so without hN the simulator could accept along a path whose induced N-run accepts only after the bound.

theorem Complexity.NTM.singleTapeSim_decidesInTime {k : ℕ} {L : Language} (N : NTM k) (hk : 1 ≤ k) {T : ℕ → ℕ} (hdec : N.DecidesInTime L T) : N.singleTapeSim.DecidesInTime L (singleTapeSimTime k T)

The single-tape simulator decides the same language within the overhead time bound.

theorem Complexity.NTM.exists_singleTape_decidesInTime {k : ℕ} {L : Language} (N : NTM k) {T : ℕ → ℕ} {c : ℕ} (hdec : N.DecidesInTime L T) (hTO : BigO T fun (x : ℕ) => x ^ c) : ∃ (N' : NTM 1) (T' : ℕ → ℕ) (c' : ℕ), N'.DecidesInTime L T' ∧ BigO T' fun (x : ℕ) => x ^ c'

Single-tape reduction. If N (with k work tapes) decides L within a polynomial time bound, then some single-work-tape machine N' decides the same L within a polynomial time bound. For k = 0 the machine is padded with a dummy work tape (pad0); for k ≥ 1 it is simulated (singleTapeSim).