TM–NTM embedding: proof internals

Helper lemmas for TM.toNTM_accepts_iff, showing that the DTM step function and the NTM trace on toNTM compute the same thing.

theorem Complexity.TM.toNTM_trace_reaches {n : ℕ} (tm : TM n) (c : Cfg n tm.Q) (T : ℕ) (choices : Fin T → Bool) : tm.reaches c (tm.toNTM.trace T choices c)

theorem Complexity.TM.toNTM_trace_choice_irrel {n : ℕ} (tm : TM n) (T : ℕ) (c : Cfg n tm.Q) (ch₁ ch₂ : Fin T → Bool) : tm.toNTM.trace T ch₁ c = tm.toNTM.trace T ch₂ c

For toNTM, the trace is independent of the choice sequence since both transition functions are identical.

theorem Complexity.TM.toNTM_trace_of_reachesIn {n : ℕ} (tm : TM n) {c c' : Cfg n tm.Q} {t T : ℕ} (h : tm.reachesIn t c c') (hhalt : tm.halted c') (hle : t ≤ T) (ch : Fin T → Bool) : tm.toNTM.trace T ch c = c'

If a DTM halts within t ≤ T steps, then toNTM.trace T reaches the same halted configuration regardless of choices.

theorem Complexity.TM.toNTM_accepts_iff {n : ℕ} (tm : TM n) (x : List Bool) : tm.Accepts x ↔ tm.toNTM.Accepts x

The DTM and its NTM embedding agree on acceptance.

theorem Complexity.TM.toNTM_decidesInTime {n : ℕ} (tm : TM n) {L : Language} {f : ℕ → ℕ} (h : tm.DecidesInTime L f) : tm.toNTM.DecidesInTime L f

If a DTM decides L in time f, then its NTM embedding also decides L in time f. This is the key internal lemma for DTIME ⊆ NTIME.

theorem Complexity.TM.work_head_reachesIn_bound {n : ℕ} (tm : TM n) {c c' : Cfg n tm.Q} {t : ℕ} (h : tm.reachesIn t c c') (i : Fin n) : (c'.work i).head ≤ (c.work i).head + t

After t steps, each work tape head is at most t plus its initial value.

theorem Complexity.TM.input_head_reachesIn_bound {n : ℕ} (tm : TM n) {c c' : Cfg n tm.Q} {t : ℕ} (h : tm.reachesIn t c c') : c'.input.head ≤ c.input.head + t

After t steps, the input head is at most t plus its initial value.

theorem Complexity.TM.output_head_reachesIn_bound {n : ℕ} (tm : TM n) {c c' : Cfg n tm.Q} {t : ℕ} (h : tm.reachesIn t c c') : c'.output.head ≤ c.output.head + t

After t steps, the output head is at most t plus its initial value.

theorem Complexity.TM.reachesIn_right_unique {n : ℕ} {tm : TM n} {t : ℕ} {c c' c'' : Cfg n tm.Q} (h₁ : tm.reachesIn t c c') (h₂ : tm.reachesIn t c c'') : c' = c''

Deterministic runs have unique endpoints: reaching two configurations in the same number of steps forces them to coincide.

theorem Complexity.TM.reaches_to_reachesIn {n : ℕ} (tm : TM n) {c c' : Cfg n tm.Q} (h : tm.reaches c c') : ∃ (t : ℕ), tm.reachesIn t c c'

Convert reaches to reachesIn.

theorem Complexity.TM.reachesIn_le_halt {n : ℕ} (tm : TM n) {c c' c_halt : Cfg n tm.Q} {t t_halt : ℕ} (hr : tm.reachesIn t c c') (hh : tm.reachesIn t_halt c c_halt) (hhalt : tm.halted c_halt) : t ≤ t_halt

If a DTM halts at step t_halt, then any reachesIn t has t ≤ t_halt.

theorem Complexity.TM.initCfg_work_head_zero {n : ℕ} (tm : TM n) (x : List Bool) (i : Fin n) : ((tm.initCfg x).work i).head = 0

Initial work tape heads are all at position 0.

theorem Complexity.TM.initCfg_input_head_zero {n : ℕ} (tm : TM n) (x : List Bool) : (tm.initCfg x).input.head = 0

The initial input head is at position zero.

theorem Complexity.TM.initCfg_output_head_zero {n : ℕ} (tm : TM n) (x : List Bool) : (tm.initCfg x).output.head = 0

The initial output head is at position zero.

theorem Complexity.TM.toNTM_isTransducer {n : ℕ} (tm : TM n) (h : tm.IsTransducer) : tm.toNTM.IsTransducer

If a DTM is a transducer, so is its NTM embedding.

theorem Complexity.TM.toNTM_decidesInSpace {n : ℕ} (tm : TM n) {L : Language} {f : ℕ → ℕ} (h : tm.DecidesInSpace L f) : tm.toNTM.DecidesInSpace L f

If a DTM decides L in space f, then its NTM embedding also decides L in space f. The uniform time bound is constructed as the maximum halting time over all inputs of each length.

theorem Complexity.TM.output_cells_zero_eq_start_of_reachesIn {n : ℕ} {tm : TM n} {t : ℕ} {c₀ c : Cfg n tm.Q} (h : tm.reachesIn t c₀ c) (h0 : c₀.output.cells 0 = Γ.start) : c.output.cells 0 = Γ.start

theorem Complexity.TM.output_cells_ne_start_of_reachesIn {n : ℕ} {tm : TM n} {t : ℕ} {c₀ c : Cfg n tm.Q} (h : tm.reachesIn t c₀ c) (hno : ∀ i ≥ 1, c₀.output.cells i ≠ Γ.start) (i : ℕ) : i ≥ 1 → c.output.cells i ≠ Γ.start

theorem Complexity.TM.input_cells_eq_of_step {n : ℕ} {tm : TM n} {c c' : Cfg n tm.Q} (hs : tm.step c = some c') : c'.input.cells = c.input.cells

theorem Complexity.TM.input_cells_eq_of_reachesIn {n : ℕ} {tm : TM n} {t : ℕ} {c₀ c : Cfg n tm.Q} (h : tm.reachesIn t c₀ c) : c.input.cells = c₀.input.cells

theorem Complexity.TM.head_le_of_reachesIn {n : ℕ} {x : List Bool} (tm : TM n) {t : ℕ} {c : Cfg n tm.Q} (hreach : tm.reachesIn t (tm.initCfg x) c) : c.input.head ≤ t ∧ c.output.head ≤ t ∧ ∀ (i : Fin n), (c.work i).head ≤ t

A tape head moves at most 1 cell per step. After t steps starting from initCfg, the head is at position ≤ t.

theorem Complexity.Tape.StartInvariant.step {n : ℕ} (tm : TM n) {c c' : Cfg n tm.Q} (hstep : tm.step c = some c') (hinp : c.input.StartInvariant) (hwork : ∀ (i : Fin n), (c.work i).StartInvariant) (hout : c.output.StartInvariant) : c'.input.StartInvariant ∧ (∀ (i : Fin n), (c'.work i).StartInvariant) ∧ c'.output.StartInvariant

The invariant is preserved across one DTM step, on every tape.

theorem Complexity.NTM.input_cells_trace {n : ℕ} (tm : NTM n) (T : ℕ) (choices : Fin T → Bool) (c : Cfg n tm.Q) : (tm.trace T choices c).input.cells = c.input.cells

NTM traces never alter input tape cells; the input tape is read-only and only its head moves.

theorem Complexity.NTM.input_head_trace_le {n : ℕ} (tm : NTM n) (T : ℕ) (choices : Fin T → Bool) (c : Cfg n tm.Q) : (tm.trace T choices c).input.head ≤ c.input.head + T

During an NTM trace, the input head increases by at most one per step.

theorem Complexity.NTM.trace_two {n : ℕ} (tm : NTM n) (choices : Fin 2 → Bool) (c : Cfg n tm.Q) : tm.trace 2 choices c = tm.trace 1 (fun (x : Fin 1) => choices ⟨1, ⋯⟩) (tm.trace 1 (fun (x : Fin 1) => choices ⟨0, ⋯⟩) c)

Split a two-step trace into two one-step traces.

theorem Complexity.NTM.trace_succ {n : ℕ} (tm : NTM n) (T : ℕ) (choices : Fin (T + 1) → Bool) (c : Cfg n tm.Q) : tm.trace (T + 1) choices c = tm.trace T (fun (i : Fin T) => choices ⟨↑i + 1, ⋯⟩) (tm.trace 1 (fun (x : Fin 1) => choices ⟨0, ⋯⟩) c)

Split the first step off a nonzero trace. If the machine is already halted, both sides reduce to the starting configuration.

theorem Complexity.NTM.trace_add_two {n : ℕ} (tm : NTM n) (T : ℕ) (choices : Fin (T + 2) → Bool) (c : Cfg n tm.Q) : tm.trace (T + 2) choices c = tm.trace T (fun (i : Fin T) => choices ⟨↑i + 2, ⋯⟩) (tm.trace 2 (fun (i : Fin 2) => choices ⟨↑i, ⋯⟩) c)

Split the first two steps off a trace.

theorem Complexity.NTM.trace_cast {n : ℕ} (tm : NTM n) {T T' : ℕ} (h : T = T') (choices : Fin T → Bool) (c : Cfg n tm.Q) : tm.trace T choices c = tm.trace T' (fun (i : Fin T') => choices (Fin.cast ⋯ i)) c

Reindex a trace along an equality of time bounds.

theorem Complexity.NTM.trace_add {n : ℕ} (tm : NTM n) (T U : ℕ) (choices : Fin (T + U) → Bool) (c : Cfg n tm.Q) : tm.trace (T + U) choices c = tm.trace U (fun (i : Fin U) => choices (Fin.natAdd T i)) (tm.trace T (fun (i : Fin T) => choices (Fin.castLE ⋯ i)) c)

Split the first T steps off a trace.

This version uses Fin.castLE/Fin.natAdd for the prefix and suffix choice sequences, which keeps later proofs away from ad-hoc dependent index casts.