retargetInput simulation — proof internals

This file contains the simulation lemmas for retargetInput M, showing that retargetInput M on a configuration where work tape k holds the "virtual input" z faithfully simulates M on input z.

Key definitions and lemmas

• retargetWrap — embed a config of M : TM k into a config of retargetInput M : TM (k+1), given a choice of real-input tape.
• retargetInput_step_commute — one step of M corresponds to one step of retargetInput M under the wrap (assuming a structural invariant on c.input: cells ≥ 1 are never Γ.start).
• retargetInput_reachesIn_of_reachesIn — multi-step simulation lifting.
• retargetInput_reachesIn_halted_of_decidesInTime — user-facing: if M decides L in time T, then retargetInput M started with z on work tape k reaches a halting configuration within T(|z|) steps with the correct output.

The startedCfg family

For phase-composed machines, the interesting entry point is not initCfg but the configuration reached after M's forced first move off the ▷ cells. startedCfg M z hne names that configuration (well-defined once qstart ≠ qhalt, which qstart_ne_qhalt_of_decidesInTime guarantees for any deciding machine), and the startedCfg_* lemmas pin down each field: state, work, and output are input-independent, while every tape sits one cell right of ▷. retargetInput_decidesVirtual_started restates the user-facing simulation from this post-start configuration.

Hoare liftings

• retargetInput_hoareTime — a HoareTime triple for M lifts to a triple for retargetInput M in which the precondition reads M's input off work tape k and the postcondition existentially recovers M's final tapes.
• retargetInput_copyInputToWorkTM_started_hoareTime, retargetInput_inputLengthPlusOneCounterTM_started_hoareTime, retargetInput_inputLengthPlusOneCounterTM_started_tracksInput_hoareTime — virtual-input instantiations of the corresponding subroutine triples.

The structural invariant

Because retargetInput M writes back the read symbol on work tape k (to preserve cells), the simulation only goes through cleanly when the current write is a no-op. This requires:

head = 0 OR read ≠ Γ.start

The second disjunct is equivalent to "cells at positions ≥ 1 never contain Γ.start". This is a structural invariant of any DTM run (since δ writes only Γw, which excludes Γ.start, and writes at cell 0 are no-ops) — captured by Tape.StartInvariant below and preserved across TM.step by Tape.StartInvariant.step.

def Complexity.TM.retargetWrap {k : ℕ} (M : TM k) (realInput : Tape) (c : Cfg k M.Q) : Cfg (k + 1) M.retargetInput.Q

Embed a Cfg k M.Q into Cfg (k+1) (retargetInput M).Q by:

• putting realInput on the real input tape (ignored by the machine),
• putting c.work i on work tape i for i < k,
• putting c.input on work tape k (the virtual input). State and output are shared.

Equations

• M.retargetWrap realInput c = { state := c.state, input := realInput, work := fun (i : Fin (k + 1)) => if h : ↑i < k then c.work ⟨↑i, h⟩ else c.input, output := c.output }

@[simp]

theorem Complexity.TM.retargetWrap_state {k : ℕ} (M : TM k) (realInput : Tape) (c : Cfg k M.Q) : (M.retargetWrap realInput c).state = c.state

The state of a wrapped configuration is the state of the wrapped M-configuration.

@[simp]

theorem Complexity.TM.retargetWrap_output {k : ℕ} (M : TM k) (realInput : Tape) (c : Cfg k M.Q) : (M.retargetWrap realInput c).output = c.output

The output tape of a wrapped configuration is the output tape of the wrapped M-configuration.

@[simp]

theorem Complexity.TM.retargetWrap_input {k : ℕ} (M : TM k) (realInput : Tape) (c : Cfg k M.Q) : (M.retargetWrap realInput c).input = realInput

The (ignored) real input tape of a wrapped configuration is exactly the supplied realInput.

theorem Complexity.TM.retargetWrap_work_lt {k : ℕ} (M : TM k) (realInput : Tape) (c : Cfg k M.Q) (i : Fin (k + 1)) (h : ↑i < k) : (M.retargetWrap realInput c).work i = c.work ⟨↑i, h⟩

For an index i < k, work tape i of a wrapped configuration is work tape i of the wrapped M-configuration.

theorem Complexity.TM.retargetWrap_work_last {k : ℕ} (M : TM k) (realInput : Tape) (c : Cfg k M.Q) : (M.retargetWrap realInput c).work ⟨k, ⋯⟩ = c.input

The last work tape (index k) of a wrapped configuration holds the wrapped M-configuration's input tape — the virtual input.

theorem Complexity.TM.retargetInput_step_commute {k : ℕ} (M : TM k) {c c' : Cfg k M.Q} (hstep : M.step c = some c') (realInput : Tape) (hinp : c.input.StartInvariant) : M.retargetInput.step (M.retargetWrap realInput c) = some (M.retargetWrap (realInput.move (idleDir realInput.read)) c')

One step of M corresponds to one step of retargetInput M through retargetWrap. The real-input tape drifts by move (idleDir · ). Requires the structural invariant on c.input (cells ≥ 1 ≠ start).

theorem Complexity.TM.retargetInput_reachesIn_of_reachesIn {k : ℕ} (M : TM k) {c c' : Cfg k M.Q} {t : ℕ} (hreach : M.reachesIn t c c') (hinp : c.input.StartInvariant) (hwork : ∀ (i : Fin k), (c.work i).StartInvariant) (hout : c.output.StartInvariant) (realInput : Tape) : ∃ (finalReal : Tape), M.retargetInput.reachesIn t (M.retargetWrap realInput c) (M.retargetWrap finalReal c')

Multi-step version: if M reaches c' in t steps, then retargetInput M reaches some config (differing from retargetWrap only in the real-input tape drift) in the same t steps.

def Complexity.TM.retargetInitCfg {k : ℕ} (M : TM k) (z : List Bool) (realInput : Tape) : Cfg (k + 1) M.retargetInput.Q

Initial configuration for retargetInput M with virtual input z on work tape k and an arbitrary realInput on the (ignored) real input tape. Work tapes 0..k-1 are empty; output is empty.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.TM.retargetInitCfg_eq_retargetWrap {k : ℕ} (M : TM k) (z : List Bool) (realInput : Tape) : M.retargetInitCfg z realInput = M.retargetWrap realInput (M.initCfg z)

retargetInitCfg M z realInput is exactly the retargetWrap of M's ordinary initial configuration on input z.

theorem Complexity.TM.retargetInput_reachesIn_halted_of_decidesInTime {k : ℕ} (M : TM k) {L : Language} {T : ℕ → ℕ} (hM : M.DecidesInTime L T) (z : List Bool) (realInput : Tape) : ∃ (c' : Cfg (k + 1) M.retargetInput.Q), ∃ t ≤ T z.length, M.retargetInput.reachesIn t (M.retargetInitCfg z realInput) c' ∧ M.retargetInput.halted c' ∧ (z ∈ L → c'.output.cells 1 = Γ.one) ∧ (z ∉ L → c'.output.cells 1 = Γ.zero)

User-facing simulation: if M decides L in time T, then retargetInput M started with z on work tape k reaches a halted configuration within T(|z|) steps whose output cell 1 indicates membership of z in L.

theorem Complexity.TM.qstart_ne_qhalt_of_decidesInTime {k : ℕ} (M : TM k) {L : Language} {T : ℕ → ℕ} (hM : M.DecidesInTime L T) : M.qstart ≠ M.qhalt

A verifier that decides a language cannot have qstart = qhalt, because the initial output cell is blank, not an accepting or rejecting bit.

noncomputable def Complexity.TM.startedCfg {k : ℕ} (M : TM k) (z : List Bool) (hne : M.qstart ≠ M.qhalt) : Cfg k M.Q

The verifier configuration after its forced first move off the start cells. For a deciding machine this is well-defined by qstart_ne_qhalt_of_decidesInTime.

Equations

• M.startedCfg z hne = (M.step (M.initCfg z)).get ⋯

theorem Complexity.TM.step_initCfg_startedCfg {k : ℕ} (M : TM k) (z : List Bool) (hne : M.qstart ≠ M.qhalt) : M.step (M.initCfg z) = some (M.startedCfg z hne)

startedCfg is the result of one deterministic verifier step from M.initCfg z.

theorem Complexity.TM.startedCfg_state_eq {k : ℕ} (M : TM k) (z₁ z₂ : List Bool) (hne : M.qstart ≠ M.qhalt) : (M.startedCfg z₁ hne).state = (M.startedCfg z₂ hne).state

The verifier state immediately after the forced first move off ▷ is independent of the concrete input string: the first step reads only the start symbols on every tape.

theorem Complexity.TM.startedCfg_work_eq {k : ℕ} (M : TM k) (z₁ z₂ : List Bool) (hne : M.qstart ≠ M.qhalt) : (M.startedCfg z₁ hne).work = (M.startedCfg z₂ hne).work

The verifier work tapes immediately after the forced first move off ▷ are independent of the concrete input string.

theorem Complexity.TM.startedCfg_output_eq {k : ℕ} (M : TM k) (z₁ z₂ : List Bool) (hne : M.qstart ≠ M.qhalt) : (M.startedCfg z₁ hne).output = (M.startedCfg z₂ hne).output

The verifier output tape immediately after the forced first move off ▷ is independent of the concrete input string.

theorem Complexity.TM.startedCfg_input_eq {k : ℕ} (M : TM k) (z : List Bool) (hne : M.qstart ≠ M.qhalt) : (M.startedCfg z hne).input = (Tape.init (List.map Γ.ofBool z)).move Dir3.right

The verifier input tape immediately after the forced first move off ▷ is the ordinary initialized input moved right to cell 1.

theorem Complexity.TM.startedCfg_work_eq_init_move_right {k : ℕ} (M : TM k) (z : List Bool) (hne : M.qstart ≠ M.qhalt) (i : Fin k) : (M.startedCfg z hne).work i = (Tape.init []).move Dir3.right

Each verifier work tape immediately after the forced first move off ▷ is a blank initialized tape moved right to cell 1.

theorem Complexity.TM.startedCfg_output_eq_init_move_right {k : ℕ} (M : TM k) (z : List Bool) (hne : M.qstart ≠ M.qhalt) : (M.startedCfg z hne).output = (Tape.init []).move Dir3.right

The verifier output tape immediately after the forced first move off ▷ is a blank initialized tape moved right to cell 1.

theorem Complexity.TM.retargetInput_decidesVirtual_started {k : ℕ} (M : TM k) {L : Language} {T : ℕ → ℕ} (hM : M.DecidesInTime L T) (z : List Bool) (realInput : Tape) : ∃ (c' : Cfg (k + 1) M.retargetInput.Q) (t : ℕ), t + 1 ≤ T z.length ∧ M.retargetInput.reachesIn t (M.retargetWrap realInput (M.startedCfg z ⋯)) c' ∧ M.retargetInput.halted c' ∧ (z ∈ L → c'.output.cells 1 = Γ.one) ∧ (z ∉ L → c'.output.cells 1 = Γ.zero)

User-facing simulation from the post-start verifier configuration.

If M decides L, then retargetInput M can start from retargetWrap of the verifier state immediately after M's first step on z, and it reaches the same accepting/rejecting output. This is the form needed by phase-composed machines whose earlier phases have already moved every tape off ▷.

theorem Complexity.TM.retargetInput_hoareTime {k : ℕ} (M : TM k) {pre post : TapePred k} {b : ℕ} (hM : M.HoareTime pre post b) (hpre_inp : ∀ (inp : Tape) (work : Fin k → Tape) (out : Tape), pre inp work out → inp.StartInvariant) (hpre_work : ∀ (inp : Tape) (work : Fin k → Tape) (out : Tape), pre inp work out → ∀ (i : Fin k), (work i).StartInvariant) (hpre_out : ∀ (inp : Tape) (work : Fin k → Tape) (out : Tape), pre inp work out → out.StartInvariant) : M.retargetInput.HoareTime (fun (_inp : Tape) (work : Fin (k + 1) → Tape) (out : Tape) => pre (work ⟨k, ⋯⟩) (fun (i : Fin k) => work ⟨↑i, ⋯⟩) out) (fun (_inp : Tape) (work : Fin (k + 1) → Tape) (out : Tape) => ∃ (vin : Tape) (innerWork : Fin k → Tape), post vin innerWork out ∧ (∀ (i : Fin k), work ⟨↑i, ⋯⟩ = innerWork i) ∧ work ⟨k, ⋯⟩ = vin) b

Hoare lifting for retargetInput: if a deterministic TM satisfies a Hoare triple on its ordinary input tape, then retargetInput satisfies the corresponding triple when that input is supplied on the last work tape. The real input tape is ignored.

theorem Complexity.TM.retargetInput_copyInputToWorkTM_started_hoareTime {k : ℕ} (idx : Fin k) (x : List Bool) : (copyInputToWorkTM idx).retargetInput.HoareTime (fun (_inp : Tape) (work : Fin (k + 1) → Tape) (out : Tape) => work ⟨k, ⋯⟩ = (Tape.init (List.map Γ.ofBool x)).move Dir3.right ∧ work ⟨↑idx, ⋯⟩ = (Tape.init []).move Dir3.right ∧ out.StartInvariant ∧ ∀ (i : Fin k), i ≠ idx → (work ⟨↑i, ⋯⟩).StartInvariant) (fun (_inp : Tape) (work : Fin (k + 1) → Tape) (_out : Tape) => (work ⟨k, ⋯⟩).cells = (Tape.init (List.map Γ.ofBool x)).cells ∧ (work ⟨k, ⋯⟩).head = x.length + 1 ∧ (work ⟨↑idx, ⋯⟩).HasBinaryPrefix x) (x.length + 1)

Virtual-input version of copyInputToWorkTM_started_hoareTime: if the virtual input is a Boolean string at head 1 and work tape idx is a blank started tape, then retargetInput (copyInputToWorkTM idx) copies that virtual input onto work tape idx within |x| + 1 steps.

theorem Complexity.TM.retargetInput_inputLengthPlusOneCounterTM_started_hoareTime {k : ℕ} (counterIdx : Fin k) (x : List Bool) : (inputLengthPlusOneCounterTM counterIdx).retargetInput.HoareTime (fun (_inp : Tape) (work : Fin (k + 1) → Tape) (out : Tape) => work ⟨k, ⋯⟩ = (Tape.init (List.map Γ.ofBool x)).move Dir3.right ∧ work ⟨↑counterIdx, ⋯⟩ = (Tape.init []).move Dir3.right ∧ out.StartInvariant ∧ ∀ (i : Fin k), i ≠ counterIdx → (work ⟨↑i, ⋯⟩).StartInvariant) (fun (_inp : Tape) (work : Fin (k + 1) → Tape) (_out : Tape) => (work ⟨↑counterIdx, ⋯⟩).HasUnaryCounter (x.length + 1) ∧ (work ⟨↑counterIdx, ⋯⟩).cells 0 = Γ.start ∧ ∀ j ≥ 1, (work ⟨↑counterIdx, ⋯⟩).cells j ≠ Γ.start) (inputLengthPlusOneCounterTime x.length)

Virtual-input version of inputLengthPlusOneCounterTM_started_hoareTime: if the virtual input is a started Boolean string and work tape counterIdx is a started blank tape, then retargetInput (inputLengthPlusOneCounterTM counterIdx) materializes a unary counter of length |x| + 1 on that tape.

theorem Complexity.TM.retargetInput_inputLengthPlusOneCounterTM_started_tracksInput_hoareTime {k : ℕ} (counterIdx : Fin k) (x : List Bool) : (inputLengthPlusOneCounterTM counterIdx).retargetInput.HoareTime (fun (_inp : Tape) (work : Fin (k + 1) → Tape) (out : Tape) => work ⟨k, ⋯⟩ = (Tape.init (List.map Γ.ofBool x)).move Dir3.right ∧ work ⟨↑counterIdx, ⋯⟩ = (Tape.init []).move Dir3.right ∧ out.StartInvariant ∧ ∀ (i : Fin k), i ≠ counterIdx → (work ⟨↑i, ⋯⟩).StartInvariant) (fun (_inp : Tape) (work : Fin (k + 1) → Tape) (_out : Tape) => (work ⟨k, ⋯⟩).cells = (Tape.init (List.map Γ.ofBool x)).cells ∧ (work ⟨k, ⋯⟩).head = x.length + 1 ∧ (work ⟨↑counterIdx, ⋯⟩).HasUnaryCounter (x.length + 1) ∧ (work ⟨↑counterIdx, ⋯⟩).cells 0 = Γ.start ∧ ∀ j ≥ 1, (work ⟨↑counterIdx, ⋯⟩).cells j ≠ Γ.start) (inputLengthPlusOneCounterTime x.length)

Virtual-input version of inputLengthPlusOneCounterTM_started_tracksInput_hoareTime: besides building the unary counter on work tape counterIdx, the postcondition also records the final cells and head of the virtual-input tape itself.