loopTM simulation — proof internals

This file contains the simulation lemmas for loopTM tmBody tmTest.

Key definitions

• loopBodyWrap — embed a tmBody config into the loopTM config space
• loopTestWrap — embed a tmTest config into the loopTM config space
• Tape transformations use the shared transitionTape / transitionInput

def Complexity.TM.loopBodyWrap {n : ℕ} (tmBody tmTest : TM n) (c : Cfg n tmBody.Q) : Cfg n (LoopQ tmBody.Q tmTest.Q)

Embed a tmBody config into the loopTM config space (body phase).

Equations

• tmBody.loopBodyWrap tmTest c = { state := Sum.inl c.state, input := c.input, work := c.work, output := c.output }

def Complexity.TM.loopTestWrap {n : ℕ} (tmBody tmTest : TM n) (c : Cfg n tmTest.Q) : Cfg n (LoopQ tmBody.Q tmTest.Q)

Embed a tmTest config into the loopTM config space (test phase).

Equations

• tmBody.loopTestWrap tmTest c = { state := Sum.inr (Sum.inr c.state), input := c.input, work := c.work, output := c.output }

theorem Complexity.TM.loopTM_body_step {n : ℕ} (tmBody tmTest : TM n) {c c' : Cfg n tmBody.Q} (hstep : tmBody.step c = some c') : (tmBody.loopTM tmTest).step (tmBody.loopBodyWrap tmTest c) = some (tmBody.loopBodyWrap tmTest c')

A non-halting tmBody step is simulated by one loopTM step on body-wrapped configurations.

theorem Complexity.TM.loopTM_body_simulation {n : ℕ} (tmBody tmTest : TM n) {t : ℕ} {c_start c_end : Cfg n tmBody.Q} (hreach : tmBody.reachesIn t c_start c_end) : (tmBody.loopTM tmTest).reachesIn t (tmBody.loopBodyWrap tmTest c_start) (tmBody.loopBodyWrap tmTest c_end)

A t-step run of tmBody lifts to a t-step run of loopTM between the body-wrapped configurations.

theorem Complexity.TM.loopTM_body_to_test {n : ℕ} (tmBody tmTest : TM n) {c : Cfg n tmBody.Q} (hhalt : c.state = tmBody.qhalt) : (tmBody.loopTM tmTest).step (tmBody.loopBodyWrap tmTest c) = some (tmBody.loopTestWrap tmTest { state := tmTest.qstart, input := transitionInput c.input, work := fun (i : Fin n) => transitionTape (c.work i), output := transitionTape c.output })

When tmBody has halted, one loopTM step moves from the body-wrapped configuration to tmTest's start state, applying the shared tape transition to every tape.

theorem Complexity.TM.loopTM_test_step {n : ℕ} (tmBody tmTest : TM n) {c c' : Cfg n tmTest.Q} (hstep : tmTest.step c = some c') : (tmBody.loopTM tmTest).step (tmBody.loopTestWrap tmTest c) = some (tmBody.loopTestWrap tmTest c')

A non-halting tmTest step is simulated by one loopTM step on test-wrapped configurations.

theorem Complexity.TM.loopTM_test_simulation {n : ℕ} (tmBody tmTest : TM n) {t : ℕ} {c_start c_end : Cfg n tmTest.Q} (hreach : tmTest.reachesIn t c_start c_end) : (tmBody.loopTM tmTest).reachesIn t (tmBody.loopTestWrap tmTest c_start) (tmBody.loopTestWrap tmTest c_end)

A t-step run of tmTest lifts to a t-step run of loopTM between the test-wrapped configurations.

theorem Complexity.TM.loopTM_test_to_rewind {n : ℕ} (tmBody tmTest : TM n) {c : Cfg n tmTest.Q} (hhalt : c.state = tmTest.qhalt) : (tmBody.loopTM tmTest).step (tmBody.loopTestWrap tmTest c) = some { state := Sum.inr (Sum.inl LoopPhase.rewindOut), input := transitionInput c.input, work := fun (i : Fin n) => transitionTape (c.work i), output := transitionTape c.output }

When tmTest has halted, one loopTM step moves from the test-wrapped configuration to the rewindOut phase, applying the shared tape transition to every tape.

theorem Complexity.TM.loopTM_rewind_loop {n : ℕ} (tmBody tmTest : TM n) (p : ℕ) (c : Cfg n (LoopQ tmBody.Q tmTest.Q)) : c.state = Sum.inr (Sum.inl LoopPhase.rewindOut) → c.output.cells 0 = Γ.start → (∀ j ≥ 1, c.output.cells j ≠ Γ.start) → c.output.head = p → ∃ (c_check : Cfg n (tmBody.loopTM tmTest).Q), (tmBody.loopTM tmTest).reachesIn (p + 1) c c_check ∧ c_check.state = Sum.inr (Sum.inl LoopPhase.check) ∧ c_check.output.head = 1 ∧ c_check.output.cells = c.output.cells

From the rewindOut phase with the output head at position p, loopTM reaches the check phase in p + 1 steps with the output head at cell 1 and the output cells unchanged.

theorem Complexity.TM.loopTM_check_halt {n : ℕ} (tmBody tmTest : TM n) (c : Cfg n (LoopQ tmBody.Q tmTest.Q)) (hstate : c.state = Sum.inr (Sum.inl LoopPhase.check)) (hhead : c.output.head = 1) (hcell1 : c.output.cells 1 = Γ.one) : ∃ (c' : Cfg n (tmBody.loopTM tmTest).Q), (tmBody.loopTM tmTest).step c = some c' ∧ c'.state = Sum.inr (Sum.inl LoopPhase.done) ∧ c'.output.cells = c.output.cells

In the check phase, if output cell 1 holds 1 then one loopTM step enters the done phase, leaving the output cells unchanged.

theorem Complexity.TM.loopTM_check_continue {n : ℕ} (tmBody tmTest : TM n) (c : Cfg n (LoopQ tmBody.Q tmTest.Q)) (hstate : c.state = Sum.inr (Sum.inl LoopPhase.check)) (hhead : c.output.head = 1) (hcell1 : c.output.cells 1 ≠ Γ.one) (hnostart : ∀ j ≥ 1, c.output.cells j ≠ Γ.start) : ∃ (c' : Cfg n (tmBody.loopTM tmTest).Q), (tmBody.loopTM tmTest).step c = some c' ∧ c'.state = Sum.inl tmBody.qstart ∧ c'.output.cells = c.output.cells

In the check phase, if output cell 1 does not hold 1 then one loopTM step restarts tmBody (state Sum.inl tmBody.qstart), leaving the output cells unchanged.

theorem Complexity.TM.loopTM_halted_done {n : ℕ} (tmBody tmTest : TM n) (c : Cfg n (LoopQ tmBody.Q tmTest.Q)) (h : c.state = Sum.inr (Sum.inl LoopPhase.done)) : (tmBody.loopTM tmTest).halted c

A loopTM configuration in the done phase is halted.

theorem Complexity.TM.loopTM_iteration_halt {n : ℕ} (tmBody tmTest : TM n) {t_body : ℕ} {c_body_start c_body_end : Cfg n tmBody.Q} (hreach_body : tmBody.reachesIn t_body c_body_start c_body_end) (hhalt_body : c_body_end.state = tmBody.qhalt) {t_test : ℕ} {c_test_end : Cfg n tmTest.Q} (hreach_test : tmTest.reachesIn t_test { state := tmTest.qstart, input := transitionInput c_body_end.input, work := fun (i : Fin n) => transitionTape (c_body_end.work i), output := transitionTape c_body_end.output } c_test_end) (hhalt_test : c_test_end.state = tmTest.qhalt) {p : ℕ} (hcell0 : (transitionTape c_test_end.output).cells 0 = Γ.start) (hnostart : ∀ j ≥ 1, (transitionTape c_test_end.output).cells j ≠ Γ.start) (hhead : (transitionTape c_test_end.output).head = p) (hcell1 : (transitionTape c_test_end.output).cells 1 = Γ.one) : ∃ (c_final : Cfg n (tmBody.loopTM tmTest).Q), (tmBody.loopTM tmTest).reachesIn (t_body + 1 + t_test + 1 + (p + 1) + 1) (tmBody.loopBodyWrap tmTest c_body_start) c_final ∧ (tmBody.loopTM tmTest).halted c_final ∧ c_final.output.cells 1 = Γ.one

One full loopTM iteration ending in halt: if tmBody halts in t_body steps, tmTest then halts in t_test steps, and the resulting output tape (head at p, cell 1 = 1, ▷ only at cell 0) passes the check, then loopTM halts from the body-wrapped start in t_body + 1 + t_test + 1 + (p + 1) + 1 steps with output cell 1 equal to 1.