Deterministic NTMs → DTMs

An NTM whose two transition functions coincide is deterministic: its trace is independent of the choice sequence and coincides with the run of the DTM NTM.toTM obtained by keeping the false transition function. This lets the multi-tape → single-tape NTM simulation (NTM.singleTapeSim) be reused for deterministic machines:

• NTM.Deterministic, NTM.toTM — the predicate and the conversion.
• NTM.toTM_decidesInTime — a deterministic NTM decider yields a toTM decider in the same time bound. NTM.DecidesInTime encodes rejection only as ¬acceptance (output cell 1 ≠ 1), while TM.DecidesInTime demands the cell be exactly 0, so the conversion also needs the output discipline NTM.RejectsWithZero (which every machine arising from a DTM satisfies).
• TM.toNTM_deterministic, NTM.pad0_deterministic, NTM.singleTapeSim_deterministic — the embedding, the padding, and the single-tape simulator all preserve determinism (the simulator consults its choice bit only to feed it to N.δ).
• TM.exists_singleTape_decidesInTime — the headline: every language decidable by a k-work-tape DTM in time T is decidable by a single-work-tape DTM within singleTapeSimTime k T = fun n => 16 * (k + 1) * (T n + n + 1) ^ 2.

def Complexity.NTM.Deterministic {n : ℕ} (N : NTM n) : Prop

An NTM is deterministic when its two transition functions coincide. The ∀ b form (rather than δ true = δ false) rewrites uniformly under any choice bit.

Equations

• N.Deterministic = ∀ (b : Bool), N.δ b = N.δ false

theorem Complexity.NTM.Deterministic.δ_eq {n : ℕ} {N : NTM n} (hdet : N.Deterministic) (b : Bool) : N.δ b = N.δ false

Unfolded form of Deterministic, usable as a rewrite rule.

def Complexity.NTM.toTM {n : ℕ} (N : NTM n) : TM n

Convert an NTM back to a DTM by keeping the false transition function. For a Deterministic machine this is a semantics-preserving inverse of TM.toNTM.

Equations

• N.toTM = { Q := N.Q, decEq := N.decEq, finQ := N.finQ, qstart := N.qstart, qhalt := N.qhalt, δ := N.δ false, δ_right_of_start := ⋯ }

theorem Complexity.NTM.Deterministic.trace_congr_choices {n : ℕ} {N : NTM n} (hdet : N.Deterministic) (T : ℕ) (c : Cfg n N.Q) (ch₁ ch₂ : Fin T → Bool) : N.trace T ch₁ c = N.trace T ch₂ c

For a deterministic NTM, the trace is independent of the choice sequence (mirror of TM.toNTM_trace_choice_irrel).

theorem Complexity.NTM.Deterministic.toTM_reachesIn_trace {n : ℕ} {N : NTM n} (hdet : N.Deterministic) (T : ℕ) (choices : Fin T → Bool) (c : Cfg n N.Q) : ∃ t ≤ T, N.toTM.reachesIn t c (N.trace T choices c)

Step-exact correspondence. The toTM run reaches the deterministic NTM's trace configuration within the trace length.

def Complexity.NTM.RejectsWithZero {n : ℕ} (N : NTM n) (L : Language) (T : ℕ → ℕ) : Prop

On every rejected input, every length-T(|x|) computation path ends with 0 at output cell 1. NTM.DecidesInTime encodes rejection only as ¬acceptance (cell ≠ 1, e.g. possibly blank), but TM.DecidesInTime demands the cell be exactly 0; this is the missing output discipline, satisfied by every machine arising from a DTM decider.

Equations

• N.RejectsWithZero L T = ∀ x ∉ L, ∀ (choices : Fin (T x.length) → Bool), (N.trace (T x.length) choices (N.initCfg x)).output.cells 1 = Complexity.Γ.zero

theorem Complexity.NTM.toTM_decidesInTime {n : ℕ} {N : NTM n} (hdet : N.Deterministic) {L : Language} {T : ℕ → ℕ} (h : N.DecidesInTime L T) (hrej : N.RejectsWithZero L T) : N.toTM.DecidesInTime L T

Deterministic NTM decider → DTM decider, same time bound. The toTM run is step-exact with the (choice-irrelevant) trace; acceptance transfers from the deciding hypothesis and rejection output from RejectsWithZero.

theorem Complexity.TM.toNTM_deterministic {n : ℕ} (M : TM n) : M.toNTM.Deterministic

A DTM's NTM embedding is deterministic: both transition functions are tm.δ.

theorem Complexity.TM.toNTM_rejectsWithZero {n : ℕ} {M : TM n} {L : Language} {T : ℕ → ℕ} (h : M.DecidesInTime L T) : M.toNTM.RejectsWithZero L T

A DTM decider's NTM embedding rejects with output 0: its trace freezes at the DTM's halting configuration, whose rejection cell is 0.

theorem Complexity.NTM.pad0_deterministic {N : NTM 0} (hdet : N.Deterministic) : N.pad0.Deterministic

Padding a 0-work-tape machine with a dummy work tape preserves determinism: pad0's transition threads the choice bit only into N.δ.

theorem Complexity.NTM.pad0_rejectsWithZero {N : NTM 0} {L : Language} {T : ℕ → ℕ} (hrej : N.RejectsWithZero L T) : N.pad0.RejectsWithZero L T

Padding preserves the zero-on-rejection output discipline (the padded machine's output tape tracks the original's verbatim).

theorem Complexity.NTM.singleTapeSim_deterministic {k : ℕ} {N : NTM k} (hdet : N.Deterministic) : N.singleTapeSim.Deterministic

The single-tape simulator of a deterministic machine is deterministic: the simulator's transition consults the choice bit only at the GATHER sentinel step, where it feeds it to N.δ.

theorem Complexity.NTM.SingleTape.haltCorr_output_cells {k : ℕ} (N : NTM k) {M : ℕ} {c1 : Cfg 1 (SimQ k N.Q)} {c : Cfg k N.Q} (hcorr : Corr N M c1 c) (hh : c.state = N.qhalt) : (N.singleTapeSim.trace 1 (fun (x : Fin 1) => false) c1).output.cells = c.output.cells

Halt-step correspondence, cells version: when N has halted, the simulator's one halt step lands with exactly N's output cells (via Corr.outputEq; strengthens halted_of_corr's accept-bit ↔).

theorem Complexity.NTM.SingleTape.halts_rev_output_cells {k : ℕ} (N : NTM k) (hk : 1 ≤ k) (ch : ℕ → Bool) (x : List Bool) (Tn : ℕ) (hhalt : (N.trace Tn (fun (i : Fin Tn) => inducedChoices k ch ↑i) (N.initCfg x)).state = N.qhalt) : ∃ m ≤ Tn * macroBound k Tn + 1, N.singleTapeSim.halted (N.singleTapeSim.trace m (fun (i : Fin m) => ch ↑i) (N.singleTapeSim.initCfg x)) ∧ (N.singleTapeSim.trace m (fun (i : Fin m) => ch ↑i) (N.singleTapeSim.initCfg x)).output.cells = (N.trace Tn (fun (i : Fin Tn) => inducedChoices k ch ↑i) (N.initCfg x)).output.cells

Reverse halting, cells version (mirrors halted_singleTapeSim_of_trace_qhalt, strengthening the accept-bit ↔ to equality of the output cells via Corr.outputEq): if the N-run induced by an arbitrary simulator stream halts within Tn steps, the simulator halts within the budget with the same output cells.

theorem Complexity.NTM.singleTapeSim_rejectsWithZero {k : ℕ} {N : NTM k} (hk : 1 ≤ k) {L : Language} {T : ℕ → ℕ} (hN : N.AllPathsHaltIn T) (hrej : N.RejectsWithZero L T) : N.singleTapeSim.RejectsWithZero L (singleTapeSimTime k T)

The single-tape simulator inherits the zero-on-rejection output discipline: the simulator's output tape tracks N's exactly (Corr.outputEq).

theorem Complexity.TM.exists_singleTape_decidesInTime {k : ℕ} (M : TM k) {L : Language} {T : ℕ → ℕ} (h : M.DecidesInTime L T) : ∃ (M₁ : TM 1), M₁.DecidesInTime L (NTM.singleTapeSimTime k T)

Single-tape reduction for DTMs. Every language decidable by a k-work-tape DTM in time T is decidable by a single-work-tape DTM within the quadratic overhead bound singleTapeSimTime k T = fun n => 16 * (k + 1) * (T n + n + 1) ^ 2. Chain: embed (toNTM), simulate (singleTapeSim, or pad0 for k = 0), convert back (toTM) via determinism.