Single-tape simulation — transition function

The phase transition functions assembled into the single-tape simulator's δ. Each phase function has the full δ-output signature SimQ k Q × (Fin 1 → Γw) × Γw × Dir3 × (Fin 1 → Dir3) × Dir3 (next state, single work write, output write, input dir, single work dir, output dir — there is no input write, the input tape being read-only).

All six phases are implemented — runStep, gatherStep, rewindStep, scatter1Step, scatter2Step, commitStep — and dispatched by simDelta, which drives the macro-step cycle run → gather → rewind → scatter1 → scatter2 → commit → run. Each phase comes with its ▷-safety lemma (*_right_of_start), and NTM.singleTapeSim packages simDelta into the 1-work-tape machine simulating a k-work-tape NTM. The file also proves the structural lemmas used by the simulation proof: choice irrelevance off the □ sentinel, phase-membership of each step's successor state, and the backward-chaining characterizations of gather and run predecessors. See docs/A4-SingleTapeSimulation.md.

def Complexity.NTM.SingleTape.runStep {k : ℕ} {Q : Type} (q : Q) (iHead wH oHead : Γ) : SimQ k Q × (Fin 1 → Γw) × Γw × Dir3 × (Fin 1 → Dir3) × Dir3

The run step starts a macro-step: read the input/output head symbols, initialise GATHER (accumulator all ▷ = the heads-at-0 default that the sweep overwrites for heads it finds; sweep at tape 0, slot 0), and reposition the work head to cell 1. idleDir wH moves the work head right off ▷ on the very first step (initial config) and stays on cell 1 afterwards; idleDir on input/output performs the ▷-dodge.

Equations

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

theorem Complexity.NTM.SingleTape.runStep_right_of_start {k : ℕ} {Q : Type} (q : Q) (iHead wH oHead : Γ) : (iHead = Γ.start → (runStep q iHead wH oHead).2.2.2.1 = Dir3.right) ∧ (∀ (i : Fin 1), wH = Γ.start → (runStep q iHead wH oHead).2.2.2.2.1 i = Dir3.right) ∧ (oHead = Γ.start → (runStep q iHead wH oHead).2.2.2.2.2 = Dir3.right)

run's directions are ▷-safe (everything is idleDir).

def Complexity.NTM.SingleTape.rewindStep {k : ℕ} {Q : Type} (d : RewindData k Q) (iHead wH oHead : Γ) : SimQ k Q × (Fin 1 → Γw) × Γw × Dir3 × (Fin 1 → Dir3) × Dir3

The rewind step sweeps the work head leftward, carrying the δ results untouched, until it reads ▷ (cell 0); then it steps right to cell 1 and enters SCATTER sweep 1 (empty carries). Moves left otherwise.

Equations

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

theorem Complexity.NTM.SingleTape.rewindStep_right_of_start {k : ℕ} {Q : Type} (d : RewindData k Q) (iHead wH oHead : Γ) : (iHead = Γ.start → (rewindStep d iHead wH oHead).2.2.2.1 = Dir3.right) ∧ (∀ (i : Fin 1), wH = Γ.start → (rewindStep d iHead wH oHead).2.2.2.2.1 i = Dir3.right) ∧ (oHead = Γ.start → (rewindStep d iHead wH oHead).2.2.2.2.2 = Dir3.right)

rewind's directions are ▷-safe: the work head moves left only off ▷ (it moves right on ▷); input/output use idleDir.

def Complexity.NTM.SingleTape.safeDir (head : Γ) (d : Dir3) : Dir3

Clamp a direction to be ▷-safe: a head reading ▷ is forced right (δ_right_of_start). On non-▷ cells (the reachable case) it is the identity, so it never changes the simulated behaviour.

Equations

• Complexity.NTM.SingleTape.safeDir head d = if head = Complexity.Γ.start then Complexity.Dir3.right else d

@[simp]

theorem Complexity.NTM.SingleTape.safeDir_start (d : Dir3) : safeDir Γ.start d = Dir3.right

safeDir on a head reading ▷ is right, whatever the requested direction.

theorem Complexity.NTM.SingleTape.safeDir_right_of_start {head : Γ} {d : Dir3} (h : head = Γ.start) : safeDir head d = Dir3.right

Hypothesis-form of safeDir_start: if the head symbol equals ▷ then safeDir clamps the direction to right.

def Complexity.NTM.SingleTape.commitStep {k : ℕ} {Q : Type} (d : CommitData Q) (iHead wH oHead : Γ) : SimQ k Q × (Fin 1 → Γw) × Γw × Dir3 × (Fin 1 → Dir3) × Dir3

The COMMIT step applies the simulated N-step's deferred input/output actions — output write+move, input move — then returns to run q' (work head idling at cell 1). It accounts for the ▷-dodge performed at run: if the original input/output symbol was ▷ that head already moved right, so we leave it (idle); otherwise we apply the recorded action, ▷-clamped.

Equations

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

theorem Complexity.NTM.SingleTape.commitStep_right_of_start {k : ℕ} {Q : Type} (d : CommitData Q) (iHead wH oHead : Γ) : (iHead = Γ.start → (commitStep d iHead wH oHead).2.2.2.1 = Dir3.right) ∧ (∀ (i : Fin 1), wH = Γ.start → (commitStep d iHead wH oHead).2.2.2.2.1 i = Dir3.right) ∧ (oHead = Γ.start → (commitStep d iHead wH oHead).2.2.2.2.2 = Dir3.right)

COMMIT's directions are ▷-safe (δ_right_of_start).

def Complexity.NTM.SingleTape.advanceSweep (k : ℕ) (pos : SweepPos k) : SweepPos k

Advance the sweep one cell within the block layout: slot 0 → 1 → 2 within a tape's triple, then on to the next tape's slot 0 (wrapping past the last tape into the next block's tape 0).

Equations

• Complexity.NTM.SingleTape.advanceSweep k pos = if pos.2 = 2 then (⟨if ↑pos.1 + 1 < k then ↑pos.1 + 1 else 0, ⋯⟩, 0) else (pos.1, pos.2 + 1)

def Complexity.NTM.SingleTape.gatherStep {k : ℕ} (N : NTM k) (b : Bool) (d : GatherData k N.Q) (iHead wH oHead : Γ) : SimQ k N.Q × (Fin 1 → Γw) × Γw × Dir3 × (Fin 1 → Dir3) × Dir3

One GATHER step. The work head sweeps rightward over the encoded region, reading each tape's (sym-hi, sym-lo, head-bit) triple and recording the symbol under a head into acc. Slots:

• 0 (sym-hi): stash the high code cell in pending.
• 1 (sym-lo): decode the symbol (decSymΓ) into pending.
• 2 (head-bit): if set (Γ.one), this tape's head is here — write the decoded symbol into acc at this tape.

Reaching the □ sentinel ends the sweep: apply N.δ b (the one meaningful use of the choice b) and hand the writes/directions to SCATTER. The work head moves right while sweeping and never left except on □ (≠ ▷), so the work direction is ▷-safe; input/output stay put via idleDir and are preserved via readBackWrite.

Equations

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

theorem Complexity.NTM.SingleTape.gatherStep_right_of_start {k : ℕ} (N : NTM k) (b : Bool) (d : GatherData k N.Q) (iHead wH oHead : Γ) : (iHead = Γ.start → (gatherStep N b d iHead wH oHead).2.2.2.1 = Dir3.right) ∧ (∀ (i : Fin 1), wH = Γ.start → (gatherStep N b d iHead wH oHead).2.2.2.2.1 i = Dir3.right) ∧ (oHead = Γ.start → (gatherStep N b d iHead wH oHead).2.2.2.2.2 = Dir3.right)

The GATHER step's directions are ▷-safe (δ_right_of_start): input and output use idleDir, and the work head moves left only on the □ sentinel (never on ▷), moving right in every ▷-reachable branch.

def Complexity.NTM.SingleTape.retreatSweep (k : ℕ) (pos : SweepPos k) : SweepPos k

Retreat the sweep one cell (leftward): slot 2 → 1 → 0, then to the previous tape's slot 2 (wrapping past tape 0 to tape k-1 of the previous block).

Equations

• Complexity.NTM.SingleTape.retreatSweep k pos = if pos.2 = 0 then (⟨if ↑pos.1 = 0 then k - 1 else ↑pos.1 - 1, ⋯⟩, 2) else (pos.1, pos.2 - 1)

def Complexity.NTM.SingleTape.scatter1Step {k : ℕ} {Q : Type} (d : Scatter1Data k Q) (iHead wH oHead : Γ) : SimQ k Q × (Fin 1 → Γw) × Γw × Dir3 × (Fin 1 → Dir3) × Dir3

One SCATTER sweep-1 step (rightward). Writes each head's new symbol, places stay/right markers (carrying right ones to the next block via rightCarry), records left-movers (isLeftMover) for sweep 2, and — on reaching the □ sentinel — materializes a fresh block (mat) before turning around (leftward) into sweep 2 once the block is complete. Directions are factored out: input/output idle, work head moves right except the single □-only turn-around, so δ_right_of_start is immediate.

Equations

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

def Complexity.NTM.SingleTape.scatter2Step {k : ℕ} {Q : Type} (d : Scatter2Data k Q) (iHead wH oHead : Γ) : SimQ k Q × (Fin 1 → Γw) × Γw × Dir3 × (Fin 1 → Dir3) × Dir3

One SCATTER sweep-2 step (leftward). Deposits the recorded left-movers (isLeftMover): clears each one's old marker and re-sets it one block left (leftCarry). On reaching ▷ (cell 0) it steps right to cell 1 and enters COMMIT. Directions factored: input/output idle, work head moves left except the ▷-only turn into COMMIT, so δ_right_of_start is immediate.

Equations

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

theorem Complexity.NTM.SingleTape.scatter1Step_right_of_start {k : ℕ} {Q : Type} (d : Scatter1Data k Q) (iHead wH oHead : Γ) : (iHead = Γ.start → (scatter1Step d iHead wH oHead).2.2.2.1 = Dir3.right) ∧ (∀ (i : Fin 1), wH = Γ.start → (scatter1Step d iHead wH oHead).2.2.2.2.1 i = Dir3.right) ∧ (oHead = Γ.start → (scatter1Step d iHead wH oHead).2.2.2.2.2 = Dir3.right)

scatter1's directions are ▷-safe.

theorem Complexity.NTM.SingleTape.scatter2Step_right_of_start {k : ℕ} {Q : Type} (d : Scatter2Data k Q) (iHead wH oHead : Γ) : (iHead = Γ.start → (scatter2Step d iHead wH oHead).2.2.2.1 = Dir3.right) ∧ (∀ (i : Fin 1), wH = Γ.start → (scatter2Step d iHead wH oHead).2.2.2.2.1 i = Dir3.right) ∧ (oHead = Γ.start → (scatter2Step d iHead wH oHead).2.2.2.2.2 = Dir3.right)

scatter2's directions are ▷-safe (work moves left only off ▷).

def Complexity.NTM.SingleTape.simDelta {k : ℕ} (N : NTM k) (b : Bool) (state : SimQ k N.Q) (iHead : Γ) (wHead : Fin 1 → Γ) (oHead : Γ) : SimQ k N.Q × (Fin 1 → Γw) × Γw × Dir3 × (Fin 1 → Dir3) × Dir3

The assembled single-tape transition function: dispatch on the phase. The work head symbol is wHead 0 (the single work tape).

Equations

• One or more equations did not get rendered due to their size.
• Complexity.NTM.SingleTape.simDelta N b (Sum.inr (Sum.inl d)) iHead wHead oHead = Complexity.NTM.SingleTape.gatherStep N b d iHead (wHead 0) oHead
• Complexity.NTM.SingleTape.simDelta N b (Sum.inr (Sum.inr (Sum.inl d))) iHead wHead oHead = Complexity.NTM.SingleTape.rewindStep d iHead (wHead 0) oHead
• Complexity.NTM.SingleTape.simDelta N b (Sum.inr (Sum.inr (Sum.inr (Sum.inl d)))) iHead wHead oHead = Complexity.NTM.SingleTape.scatter1Step d iHead (wHead 0) oHead
• Complexity.NTM.SingleTape.simDelta N b (Sum.inr (Sum.inr (Sum.inr (Sum.inr (Sum.inl d))))) iHead wHead oHead = Complexity.NTM.SingleTape.scatter2Step d iHead (wHead 0) oHead
• Complexity.NTM.SingleTape.simDelta N b (Sum.inr (Sum.inr (Sum.inr (Sum.inr (Sum.inr (Sum.inl d)))))) iHead wHead oHead = Complexity.NTM.SingleTape.commitStep d iHead (wHead 0) oHead

theorem Complexity.NTM.SingleTape.simDelta_right_of_start {k : ℕ} (N : NTM k) (b : Bool) (q : SimQ k N.Q) (iHead : Γ) (wHeads : Fin 1 → Γ) (oHead : Γ) : (iHead = Γ.start → (simDelta N b q iHead wHeads oHead).2.2.2.1 = Dir3.right) ∧ (∀ (i : Fin 1), wHeads i = Γ.start → (simDelta N b q iHead wHeads oHead).2.2.2.2.1 i = Dir3.right) ∧ (oHead = Γ.start → (simDelta N b q iHead wHeads oHead).2.2.2.2.2 = Dir3.right)

The assembled transition satisfies δ_right_of_start: every phase moves a head reading ▷ to the right. Each case is the corresponding phase's *_right_of_start; the work-head condition uses wHeads i = wHeads 0 (Fin 1 is a subsingleton).

theorem Complexity.NTM.SingleTape.gatherStep_eq_of_ne_blank {k : ℕ} (N : NTM k) (b b' : Bool) (d : GatherData k N.Q) (iHead wH oHead : Γ) (h : wH ≠ Γ.blank) : gatherStep N b d iHead wH oHead = gatherStep N b' d iHead wH oHead

Choice irrelevance — GATHER step. Off the □ sentinel, the GATHER step does not consult the nondeterministic bit b (only the sentinel step fires N.δ b), so it produces the same output under any choice.

theorem Complexity.NTM.SingleTape.gatherStep_fst_eq_gather_of_ne_blank {k : ℕ} (N : NTM k) (b : Bool) (d : GatherData k N.Q) (iHead wH oHead : Γ) (h : wH ≠ Γ.blank) : ∃ (d' : GatherData k N.Q), (gatherStep N b d iHead wH oHead).1 = SimQ.gather d'

GATHER stays in GATHER off the sentinel. As long as the work head is not on the □ sentinel, the GATHER step's next state is again a GATHER state (the sweep only leaves GATHER to enter REWIND when it reads □). The inductive building block for characterizing the sweep's per-step states.

theorem Complexity.NTM.SingleTape.gatherStep_snd_eq_of_ne_blank {k : ℕ} (N : NTM k) (b : Bool) (d : GatherData k N.Q) (iHead wH oHead : Γ) (h : wH ≠ Γ.blank) : ((gatherStep N b d iHead wH oHead).2.1 = fun (x : Fin 1) => TM.readBackWrite wH) ∧ (gatherStep N b d iHead wH oHead).2.2.1 = TM.readBackWrite oHead ∧ (gatherStep N b d iHead wH oHead).2.2.2.1 = TM.idleDir iHead ∧ ((gatherStep N b d iHead wH oHead).2.2.2.2.1 = fun (x : Fin 1) => Dir3.right) ∧ (gatherStep N b d iHead wH oHead).2.2.2.2.2 = TM.idleDir oHead

GATHER non-state components off the sentinel. For wH ≠ □ all three sweep sub-branches (head-bit / sym-hi / sym-lo) agree on everything but the next state: the work head reads-back-writes wH and moves right, input/output stay idle. Lets the per-step sweep lemma treat one gather step uniformly.

theorem Complexity.NTM.SingleTape.eq_run_or_gather_of_simDelta_eq_gather {k : ℕ} (N : NTM k) (b : Bool) (state : SimQ k N.Q) (iHead : Γ) (wHead : Fin 1 → Γ) (oHead : Γ) (d' : GatherData k N.Q) (h : (simDelta N b state iHead wHead oHead).1 = SimQ.gather d') : (∃ (q : N.Q), state = SimQ.run q) ∨ ∃ (d : GatherData k N.Q), state = SimQ.gather d

A GATHER configuration arises only from run or gather. The only transitions producing a GATHER state are run → gather (starting the sweep) and gather → gather (continuing it); every back-phase step (rewind/scatter1/scatter2/commit) and halt produces a non-GATHER state. The backward-chaining tool for locating the sweep within a macro-step.

theorem Complexity.NTM.SingleTape.eq_commit_of_simDelta_eq_run {k : ℕ} (N : NTM k) (b : Bool) (state : SimQ k N.Q) (iHead : Γ) (wHead : Fin 1 → Γ) (oHead : Γ) (q' : N.Q) (h : (simDelta N b state iHead wHead oHead).1 = SimQ.run q') : ∃ (d : CommitData N.Q), state = SimQ.commit d

A run configuration arises only from commit. The only transition producing a run state is commit → run (closing a macro-step); run itself steps to gather/halt, and every other phase step stays within its own cluster. Companion to eq_run_or_gather_of_simDelta_eq_gather; together they fix the phase order … → scatter2 → commit → run → gather → … of the simulation.

theorem Complexity.NTM.SingleTape.scatter1Step_fst_eq_scatter1_or_scatter2 {k : ℕ} {Q : Type} (d : Scatter1Data k Q) (iHead wH oHead : Γ) : (∃ (d' : Scatter1Data k Q), (scatter1Step d iHead wH oHead).1 = SimQ.scatter1 d') ∨ ∃ (d' : Scatter2Data k Q), (scatter1Step d iHead wH oHead).1 = SimQ.scatter2 d'

SCATTER-1 lands in scatter1 or scatter2. One sweep-1 step either continues the rightward materialization (scatter1) or, on completing the new block, turns around into sweep-2 (scatter2) — never any other phase.

theorem Complexity.NTM.SingleTape.scatter2Step_fst_eq_scatter2_or_commit {k : ℕ} {Q : Type} (d : Scatter2Data k Q) (iHead wH oHead : Γ) : (∃ (d' : Scatter2Data k Q), (scatter2Step d iHead wH oHead).1 = SimQ.scatter2 d') ∨ ∃ (d' : CommitData Q), (scatter2Step d iHead wH oHead).1 = SimQ.commit d'

SCATTER-2 lands in scatter2 or commit. One sweep-2 step either continues the leftward deposit (scatter2) or, on reaching ▷, enters commit — never any other phase.

theorem Complexity.NTM.SingleTape.simDelta_eq_of_forall_ne_blank {k : ℕ} (N : NTM k) (b b' : Bool) (state : SimQ k N.Q) (iHead : Γ) (wHead : Fin 1 → Γ) (oHead : Γ) (h : ∀ (d : GatherData k N.Q), state = SimQ.gather d → wHead 0 ≠ Γ.blank) : simDelta N b state iHead wHead oHead = simDelta N b' state iHead wHead oHead

Choice irrelevance — one simulator step. The single-tape simulator's transition consults the nondeterministic bit only at a GATHER step reading the □ sentinel (the COMPUTE sub-step firing N.δ b); every other configuration steps identically under any choice.

noncomputable def Complexity.NTM.singleTapeSim {k : ℕ} (N : NTM k) : NTM 1

The single-work-tape machine simulating the k-work-tape machine N. It stores the k work tapes block-encoded (binary, □-sentinel) on its one work tape and simulates each N-step by the phase machine run → gather → rewind → scatter1 → scatter2 → commit (see this file and docs/A4-SingleTapeSimulation.md). The Fintype/DecidableEq instances on the state type SingleTape.SimQ are noncomputable.

Equations

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