seqTM simulation — proof internals

This file contains the simulation lemmas for seqTM tm₁ tm₂.

Key definitions

• phase1Wrap — embed a tm₁ config into the seqTM config space
• phase2Wrap — embed a tm₂ config into the seqTM config space
• Tape transformations use the shared transitionTape / transitionInput

def Complexity.TM.phase1Wrap {n : ℕ} (tm₁ tm₂ : TM n) (c₁ : Cfg n tm₁.Q) : Cfg n (SeqQ tm₁.Q tm₂.Q)

Embed a tm₁ configuration into the seqTM config space (Phase 1). State is wrapped in Sum.inl; tapes are shared.

Equations

• tm₁.phase1Wrap tm₂ c₁ = { state := Sum.inl c₁.state, input := c₁.input, work := c₁.work, output := c₁.output }

def Complexity.TM.phase2Wrap {n : ℕ} (tm₁ tm₂ : TM n) (c₂ : Cfg n tm₂.Q) : Cfg n (SeqQ tm₁.Q tm₂.Q)

Embed a tm₂ configuration into the seqTM config space (Phase 2). State is wrapped in Sum.inr; tapes are shared.

Equations

• tm₁.phase2Wrap tm₂ c₂ = { state := Sum.inr c₂.state, input := c₂.input, work := c₂.work, output := c₂.output }

theorem Complexity.TM.seqTM_phase1_step {n : ℕ} (tm₁ tm₂ : TM n) {c₁ c₁' : Cfg n tm₁.Q} (hstep : tm₁.step c₁ = some c₁') : (tm₁.seqTM tm₂).step (tm₁.phase1Wrap tm₂ c₁) = some (tm₁.phase1Wrap tm₂ c₁')

One step of tm₁ corresponds to one step of seqTM during Phase 1.

theorem Complexity.TM.seqTM_reachesIn_phase1Wrap {n : ℕ} (tm₁ tm₂ : TM n) {t : ℕ} {c₁_start c₁_end : Cfg n tm₁.Q} (hreach : tm₁.reachesIn t c₁_start c₁_end) : (tm₁.seqTM tm₂).reachesIn t (tm₁.phase1Wrap tm₂ c₁_start) (tm₁.phase1Wrap tm₂ c₁_end)

Multi-step Phase 1 simulation.

theorem Complexity.TM.seqTM_transition_step {n : ℕ} (tm₁ tm₂ : TM n) {c₁ : Cfg n tm₁.Q} (hhalt : c₁.state = tm₁.qhalt) : (tm₁.seqTM tm₂).step (tm₁.phase1Wrap tm₂ c₁) = some (tm₁.phase2Wrap tm₂ { state := tm₂.qstart, input := transitionInput c₁.input, work := fun (i : Fin n) => transitionTape (c₁.work i), output := transitionTape c₁.output })

When tm₁ halts, one step of seqTM transitions to Phase 2.

theorem Complexity.TM.seqTM_phase2_step {n : ℕ} (tm₁ tm₂ : TM n) {c₂ c₂' : Cfg n tm₂.Q} (hstep : tm₂.step c₂ = some c₂') : (tm₁.seqTM tm₂).step (tm₁.phase2Wrap tm₂ c₂) = some (tm₁.phase2Wrap tm₂ c₂')

One step of tm₂ corresponds to one step of seqTM during Phase 2.

theorem Complexity.TM.seqTM_reachesIn_phase2Wrap {n : ℕ} (tm₁ tm₂ : TM n) {t : ℕ} {c₂_start c₂_end : Cfg n tm₂.Q} (hreach : tm₂.reachesIn t c₂_start c₂_end) : (tm₁.seqTM tm₂).reachesIn t (tm₁.phase2Wrap tm₂ c₂_start) (tm₁.phase2Wrap tm₂ c₂_end)

Multi-step Phase 2 simulation.

theorem Complexity.TM.seqTM_reachesIn_of_reachesIn {n : ℕ} (tm₁ tm₂ : TM n) {t₁ : ℕ} {c₁_start c₁_end : Cfg n tm₁.Q} (hreach₁ : tm₁.reachesIn t₁ c₁_start c₁_end) (hhalt₁ : c₁_end.state = tm₁.qhalt) {t₂ : ℕ} {c₂_end : Cfg n tm₂.Q} (hreach₂ : tm₂.reachesIn t₂ { state := tm₂.qstart, input := transitionInput c₁_end.input, work := fun (i : Fin n) => transitionTape (c₁_end.work i), output := transitionTape c₁_end.output } c₂_end) : (tm₁.seqTM tm₂).reachesIn (t₁ + 1 + t₂) (tm₁.phase1Wrap tm₂ c₁_start) (tm₁.phase2Wrap tm₂ c₂_end)

Full seqTM simulation combining all three phases.

theorem Complexity.TM.phase2Wrap_halted_iff {n : ℕ} (tm₁ tm₂ : TM n) (c₂ : Cfg n tm₂.Q) : (tm₁.seqTM tm₂).halted (tm₁.phase2Wrap tm₂ c₂) ↔ tm₂.halted c₂

A Phase-2 wrapped configuration is halted in seqTM iff the underlying tm₂ configuration is halted.

theorem Complexity.TM.phase2Wrap_output {n : ℕ} (tm₁ tm₂ : TM n) (c₂ : Cfg n tm₂.Q) : (tm₁.phase2Wrap tm₂ c₂).output = c₂.output

Wrapping a tm₂ configuration into the seqTM config space leaves the output tape unchanged.