The sentinel step moves heads and nothing else

Every machine begins with all heads on ▷, and TM.δ_right_of_start forces that first transition to move each of them right. Since cell zero is immutable, the transition's writes are no-ops, so the step's whole effect is to move every head from cell zero to cell one — the control state it lands in, TM.retargetInputStartState, being determined by the machine alone.

TM.startedCfg records this for the canonical initial configuration, where every work tape is blank. But the reads are ▷ on every tape whatever the tapes hold beyond cell zero, so the same description holds from any configuration with its heads at zero. That generality is what lets a composed machine hand a simulation an already-loaded work tape — a counter, say — and still enter it at the state TM.retargetInputStarted expects.

Main results

• TM.step_of_heads_zero — the sentinel step from any all-heads-at-zero configuration
• TM.startedTM — a machine resumed after that step, ready to be a stage of a composed machine
• TM.reachesIn_of_startedTM, TM.reachesIn_startedTM — the two machines reach the same configurations
• TM.reachesIn_succ_of_startedTM — a run of the resumed machine is a run of the original
• TM.step_input_cells, TM.reachesIn_input_cells — the input tape is read-only
• TM.startInvariant_reachesIn — the left-marker invariant survives a whole run
• TM.step_work_cells_ne — a step writes only under its head
• TM.head_transitionTape_le_max, TM.head_transitionInput_le_max — a phase transition never pushes a head outward
• TM.startInvariant_transitionTape, TM.startInvariant_transitionInput — and preserves the left-marker invariant

theorem Complexity.TM.writeAndMove_of_head_zero (t : Tape) (s : Γ) (d : Dir3) (h : t.head = 0) : t.writeAndMove s d = t.move d

A write at cell zero is a no-op, so writing and moving there is just moving.

theorem Complexity.TM.step_of_heads_zero {k : ℕ} (M : TM k) (c : Cfg k M.Q) (hstate : c.state = M.qstart) (hne : M.qstart ≠ M.qhalt) (hin : c.input.head = 0) (hwork : ∀ (i : Fin k), (c.work i).head = 0) (hout : c.output.head = 0) (hin0 : c.input.cells 0 = Γ.start) (hwork0 : ∀ (i : Fin k), (c.work i).cells 0 = Γ.start) (hout0 : c.output.cells 0 = Γ.start) : M.step c = some { state := M.retargetInputStartState, input := c.input.move Dir3.right, work := fun (i : Fin k) => (c.work i).move Dir3.right, output := c.output.move Dir3.right }

The sentinel step, from any configuration whose heads are at cell zero. Only the heads move; every tape keeps its contents, and the state reached is the machine's own TM.retargetInputStartState.

def Complexity.TM.startedTM {k : ℕ} (M : TM k) : TM k

A machine resumed after its sentinel step. Same transition function, same halt state; only the start state is moved forward to where the compulsory ▷-step lands. This is the form a machine has to take to be run as a stage of a composed machine, which can never hand it a head at cell zero.

Unlike TM.retargetInputStarted this leaves the input tape alone. That is the right choice when the composed machine's own input tape already carries what the stage should read: it is parked at cell one, which is exactly where the sentinel step would have left it.

Equations

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

@[simp]

theorem Complexity.TM.startedTM_qhalt {k : ℕ} (M : TM k) : M.startedTM.qhalt = M.qhalt

@[simp]

theorem Complexity.TM.startedTM_step {k : ℕ} (M : TM k) (c : Cfg k M.Q) : M.startedTM.step c = M.step c

Resuming changes no transition, so the two machines step identically.

theorem Complexity.TM.reachesIn_of_startedTM {k : ℕ} (M : TM k) {t : ℕ} {c c' : Cfg k M.startedTM.Q} (h : M.startedTM.reachesIn t c c') : M.reachesIn t c c'

…and therefore reach exactly the same configurations.

theorem Complexity.TM.reachesIn_startedTM {k : ℕ} (M : TM k) {t : ℕ} {c c' : Cfg k M.Q} (h : M.reachesIn t c c') : M.startedTM.reachesIn t c c'

…and conversely.

theorem Complexity.TM.reachesIn_succ_of_startedTM {k : ℕ} (M : TM k) (c : Cfg k M.Q) (hstate : c.state = M.qstart) (hne : M.qstart ≠ M.qhalt) (hin : c.input.head = 0) (hwork : ∀ (i : Fin k), (c.work i).head = 0) (hout : c.output.head = 0) (hin0 : c.input.cells 0 = Γ.start) (hwork0 : ∀ (i : Fin k), (c.work i).cells 0 = Γ.start) (hout0 : c.output.cells 0 = Γ.start) {t : ℕ} {c' : Cfg k M.Q} (hreach : M.startedTM.reachesIn t { state := M.startedTM.qstart, input := c.input.move Dir3.right, work := fun (i : Fin k) => (c.work i).move Dir3.right, output := c.output.move Dir3.right } c') : M.reachesIn (t + 1) c c'

What the resumed machine's start state is worth. A configuration with every head at cell zero steps, in one move, to the resumed machine's own start configuration on the same tapes with every head at cell one. So a run of the resumed machine from there is a run of the original, one step in — with whatever the tapes were carrying still on them.

theorem Complexity.TM.step_input_cells {k : ℕ} (M : TM k) {c c' : Cfg k M.Q} (h : M.step c = some c') : c'.input.cells = c.input.cells

The input tape is read-only. A transition moves its head and nothing else, so its contents survive any run — which is what lets a stage rewind the real input and hand the next stage the tape it started with.

theorem Complexity.TM.reachesIn_input_cells {k : ℕ} (M : TM k) {t : ℕ} {c c' : Cfg k M.Q} (h : M.reachesIn t c c') : c'.input.cells = c.input.cells

…and therefore across a whole run.

theorem Complexity.TM.startInvariant_reachesIn {n : ℕ} (tm : TM n) {t : ℕ} {c c' : Cfg n tm.Q} (h : tm.reachesIn t c c') : c.input.StartInvariant → (∀ (i : Fin n), (c.work i).StartInvariant) → c.output.StartInvariant → c'.input.StartInvariant ∧ (∀ (i : Fin n), (c'.work i).StartInvariant) ∧ c'.output.StartInvariant

The left-marker invariant survives a whole run, not just one step. Every transition writes symbols drawn from Γw, and cell zero is immutable, so a machine can neither erase a marker nor create one.

theorem Complexity.TM.step_work_cells_ne {k : ℕ} (M : TM k) {c c' : Cfg k M.Q} (h : M.step c = some c') (j : Fin k) (i : ℕ) (hi : i ≠ (c.work j).head) : (c'.work j).cells i = (c.work j).cells i

A step writes only under the head. Every other cell of a work tape is left alone.

theorem Complexity.TM.head_transitionTape_le_max {t : Tape} (h : t.StartInvariant) : (transitionTape t).head ≤ max t.head 1

A phase transition never pushes a head outward. On a tape carrying its marker only at cell zero it moves a head sitting on the marker to cell one and leaves every other head alone, so the head ends at max head 1. The library's bound of head + 1 is too weak to survive a loop.

theorem Complexity.TM.head_transitionInput_le_max {t : Tape} (h : t.StartInvariant) : (transitionInput t).head ≤ max t.head 1

The same for the input tape, which a transition only moves.

theorem Complexity.TM.startInvariant_transitionTape {t : Tape} (h : t.StartInvariant) : (transitionTape t).StartInvariant

A phase transition preserves the left-marker invariant.

theorem Complexity.TM.startInvariant_transitionInput {t : Tape} (h : t.StartInvariant) : (transitionInput t).StartInvariant

…and so does the input tape's.

theorem Complexity.TM.reachesIn_prefix {k : ℕ} (M : TM k) {t t' : ℕ} {c d d' : Cfg k M.Q} : M.reachesIn t c d → M.reachesIn t' c d' → t ≤ t' → M.reachesIn (t' - t) d d'

Runs from the same configuration are prefixes of one another. A deterministic machine has only one future, so a shorter run is an initial segment of a longer one. This is what lets a loop's space argument work one iteration at a time: any configuration a run passes through either lies inside the current iteration or is reached through the next iteration's start.