Moving left unconditionally

Before scratch tapes can be wiped (TM.wipeStepTM scans rightward), every head needs to be at a known position. The ▷ marker at cell 0 is immutable, so moving left far enough always reaches it whatever the content: TM.moveLeftStepTM, run enough times, is a content-agnostic bulk rewind for a whole list of tapes, exactly as TM.wipeStepTM is a content-agnostic bulk wipe.

Main results

• TM.moveLeftStepTM — move every targeted tape one cell left
• TM.moveLeftStepTM_hoareTime — its one-step contract

theorem Complexity.TM.writeAndMove_readBack_of_startInvariant (t : Tape) (h : t.StartInvariant) (d : Dir3) : t.writeAndMove (readBackWrite t.read).toΓ d = t.move d

Unconditional write-then-move collapses to a pure move whenever the tape's only possible ▷ is at cell 0 — regardless of whether the head is currently on it.

def Complexity.TM.moveLeftStepTM {n : ℕ} (targets : List (Fin n)) : TM n

One unconditional step: every work tape named in targets moves left (bouncing off ▷ via moveLeftDir); every other work tape, the input, and the output are held by readBackWrite/idleDir. Content is always preserved.

Equations

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

theorem Complexity.TM.moveLeftStepTM_hoareTime {n : ℕ} (targets : List (Fin n)) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hinp : Parked inp₀) (hout : Parked out₀) (htarget : ∀ i ∈ targets, (work₀ i).StartInvariant) (hother : ∀ i ∉ targets, Parked (work₀ i)) : (moveLeftStepTM targets).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ out = out₀ ∧ ∀ (i : Fin n), work i = if i ∈ targets then (work₀ i).move (moveLeftDir (work₀ i).read) else work₀ i) 1

moveLeftStepTM's exact one-step Hoare contract. Targeted tapes need only StartInvariant (their ▷, if any, is at cell 0 — true regardless of current head position); every other work tape, the input, and the output must be Parked.